Goal Menu:

Conjunction Command

If you select a goal of the form P1P2∧…∧Pn and give the Conjunction command, then Proof Designer will say that you now have to prove all of the statements P1, P2, …, Pn, and it will say that once these have been proven, they can be used to infer the goal. If you already have some of these statements in your givens list, then you can select them too before giving the Conjunction command. Proof Designer will then require you to prove only those statements that are not already in your givens list.

Parentheses in your goal can affect how the Conjunction command works. For example, if you select a goal of the form PQR and give the Conjunction command, then Proof Designer will say that you must prove P, 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 P and QR. Thus, you may want to add or remove parentheses in your goal before using the Conjunction command. Too add or remove parentheses, use the Reexpress command.