P. 8 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 701-800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mpanl12 701	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	mpanr1 702	An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	mpanr2 703	An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜒    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mpanr12 704	An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mpanlr1 705	An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜓    &   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	mpbirand 706	Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	mpbiran2d 707	Detach truth from conjunction in biconditional. Deduction form. (Contributed by Peter Mazsa, 24-Sep-2022.)
⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	mpbiran 708	Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)
⊢ 𝜓    &   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 ↔ 𝜒)
Theorem	mpbiran2 709	Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)
⊢ 𝜒    &   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	mpbir2an 710	Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ 𝜑
Theorem	mpbi2and 711	Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mpbir2and 712	Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	adantll 713	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)
Theorem	adantlr 714	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
Theorem	adantrl 715	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)
Theorem	adantrr 716	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)
Theorem	adantlll 717	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	adantllr 718	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	adantlrl 719	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)
Theorem	adantlrr 720	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)
Theorem	adantrll 721	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ ((𝜏 ∧ 𝜓) ∧ 𝜒)) → 𝜃)
Theorem	adantrlr 722	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜏) ∧ 𝜒)) → 𝜃)
Theorem	adantrrl 723	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜏 ∧ 𝜒))) → 𝜃)
Theorem	adantrrr 724	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜏))) → 𝜃)
Theorem	ad2antrr 725	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)
Theorem	ad2antlr 726	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)
Theorem	ad2antrl 727	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)
Theorem	ad2antll 728	Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)
Theorem	ad3antrrr 729	Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Theorem	ad3antlr 730	Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Theorem	ad4antr 731	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Theorem	ad4antlr 732	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Theorem	ad5antr 733	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Theorem	ad5antlr 734	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Theorem	ad6antr 735	Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Theorem	ad6antlr 736	Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Theorem	ad7antr 737	Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Theorem	ad7antlr 738	Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Theorem	ad8antr 739	Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)
Theorem	ad8antlr 740	Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)
Theorem	ad9antr 741	Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓)
Theorem	ad9antlr 742	Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓)
Theorem	ad10antr 743	Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓)
Theorem	ad10antlr 744	Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓)
Theorem	ad2ant2l 745	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)
Theorem	ad2ant2r 746	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)
Theorem	ad2ant2lr 747	Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)
Theorem	ad2ant2rl 748	Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒)
Theorem	adantl3r 749	Deduction adding 1 conjunct to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	ad4ant13 750	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)
Theorem	ad4ant14 751	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)
Theorem	ad4ant23 752	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒)
Theorem	ad4ant24 753	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒)
Theorem	adantl4r 754	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ (((((𝜑 ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ ((((((𝜑 ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	ad5ant12 755	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜒)
Theorem	ad5ant13 756	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) → 𝜒)
Theorem	ad5ant14 757	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒)
Theorem	ad5ant15 758	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒)
Theorem	ad5ant23 759	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) → 𝜒)
Theorem	ad5ant24 760	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒)
Theorem	ad5ant25 761	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒)
Theorem	adantl5r 762	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((((((𝜑 ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ (((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	adantl6r 763	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ (((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ ((((((((𝜑 ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	pm3.33 764	Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜒)) → (𝜑 → 𝜒))
Theorem	pm3.34 765	Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜓 → 𝜒) ∧ (𝜑 → 𝜓)) → (𝜑 → 𝜒))
Theorem	simpll 766	Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
Theorem	simplld 767	Deduction form of simpll 766, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simplr 768	Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
Theorem	simplrd 769	Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simprl 770	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜓)
Theorem	simprld 771	Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simprr 772	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜒)
Theorem	simprrd 773	Deduction form of simprr 772, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	simplll 774	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof shortened by Wolf Lammen, 6-Apr-2022.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
Theorem	simpllr 775	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof shortened by Wolf Lammen, 6-Apr-2022.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
Theorem	simplrl 776	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)
Theorem	simplrr 777	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)
Theorem	simprll 778	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)
Theorem	simprlr 779	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)
Theorem	simprrl 780	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)
Theorem	simprrr 781	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)
Theorem	simp-4l 782	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Theorem	simp-4r 783	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Theorem	simp-5l 784	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Theorem	simp-5r 785	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Theorem	simp-6l 786	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)
Theorem	simp-6r 787	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Theorem	simp-7l 788	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜑)
Theorem	simp-7r 789	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Theorem	simp-8l 790	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜑)
Theorem	simp-8r 791	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Theorem	simp-9l 792	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜑)
Theorem	simp-9r 793	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)
Theorem	simp-10l 794	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜑)
Theorem	simp-10r 795	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓)
Theorem	simp-11l 796	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜑)
Theorem	simp-11r 797	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓)
Theorem	pm2.01da 798	Deduction based on reductio ad absurdum. See pm2.01 192. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm2.18da 799	Deduction based on reductio ad absurdum. See pm2.18 128. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	impbida 800	Deduce an equivalence from two implications. Variant of impbid 215. (Contributed by NM, 17-Feb-2007.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))