Infer Menu:

Conjoin Command

Select givens P and Q and give the Conjoin command, and Proof Designer will infer PQ. You can select more than two givens, and Proof Designer will infer the conjunction of all of them.

You can also use this command to work backwards from your goal. If your goal is a statement of the form P1P2∧…∧Pn and some of the statements P1, P2, …, Pn are in your givens list, then you can select those givens and the goal and give the Conjoin command. Proof Designer will then require you to prove those conjuncts that are not already in your givens list.

Parentheses in your goal can affect how the Conjoin command works. For example, if you select a given P and a goal of the form PQR and give the Conjoin command, then Proof Designer will say that you must prove Q and R in order to complete the proof. But if the goal is P∧(QR), then Proof Designer will say that you must prove QR. Thus, you may want to add or remove parentheses in your goal before using the Conjoin command. Too add or remove parentheses, use the Reexpress command.