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	mpidan 701	A deduction which "stacks" a hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.) (Proof shortened by Wolf Lammen, 28-Mar-2021.)
⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mpan 702	An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜑    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	mpan2 703	An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mp2an 704	An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	mp4an 705	An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ 𝜏
Theorem	mpan2d 706	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	mpand 707	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜃))
Theorem	mpani 708	An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ 𝜓    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜃))
Theorem	mpan2i 709	An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ 𝜒    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	mp2ani 710	An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mp2and 711	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mpanl1 712	An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜑    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	mpanl2 713	An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 𝜓    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	mpanl12 714	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	mpanr1 715	An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	mpanr2 716	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 717	An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mpanlr1 718	An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜓    &   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	pm5.74da 719	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 4-May-2007.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
Theorem	pm4.45 720	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∧ (𝜑 ∨ 𝜓)))
Theorem	imdistan 721	Distribution of implication with conjunction. (Contributed by NM, 31-May-1999.) (Proof shortened by Wolf Lammen, 6-Dec-2012.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)))
Theorem	imdistani 722	Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))
Theorem	imdistanri 723	Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝜒 ∧ 𝜑))
Theorem	imdistand 724	Distribution of implication with conjunction (deduction rule). (Contributed by NM, 27-Aug-2004.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))
Theorem	imdistanda 725	Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))
Theorem	anbi2i 726	Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))
Theorem	anbi1i 727	Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
Theorem	anbi2ci 728	Variant of anbi2i 726 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
Theorem	anbi12i 729	Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
Theorem	anbi12ci 730	Variant of anbi12i 729 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))
Theorem	syldanl 731	A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)
Theorem	sylan9bb 732	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜒 ↔ 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))
Theorem	sylan9bbr 733	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜒 ↔ 𝜏))    ⇒   ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏))
Theorem	orbi2d 734	Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))
Theorem	orbi1d 735	Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
Theorem	anbi2d 736	Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒)))
Theorem	anbi1d 737	Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))
Theorem	orbi1 738	Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)))
Theorem	anbi1 739	Introduce a right conjunct to both sides of a logical equivalence. Theorem *4.36 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)))
Theorem	anbi2 740	Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 16-Nov-2013.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓)))
Theorem	bitr 741	Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜓 ↔ 𝜒)) → (𝜑 ↔ 𝜒))
Theorem	orbi12d 742	Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
Theorem	anbi12d 743	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
Theorem	pm5.3 744	Theorem *5.3 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)))
Theorem	pm5.61 745	Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ 𝜓) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	adantll 746	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)
Theorem	adantlr 747	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
Theorem	adantrl 748	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)
Theorem	adantrr 749	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)
Theorem	adantlll 750	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	adantllr 751	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	adantlrl 752	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)
Theorem	adantlrr 753	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)
Theorem	adantrll 754	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ ((𝜏 ∧ 𝜓) ∧ 𝜒)) → 𝜃)
Theorem	adantrlr 755	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜏) ∧ 𝜒)) → 𝜃)
Theorem	adantrrl 756	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜏 ∧ 𝜒))) → 𝜃)
Theorem	adantrrr 757	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜏))) → 𝜃)
Theorem	ad2antrr 758	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)
Theorem	ad2antlr 759	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)
Theorem	ad2antrl 760	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)
Theorem	ad2antll 761	Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)
Theorem	ad3antrrr 762	Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Theorem	ad3antlr 763	Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Theorem	ad4antr 764	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Theorem	ad4antlr 765	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Theorem	ad5antr 766	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Theorem	ad5antlr 767	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Theorem	ad6antr 768	Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Theorem	ad6antlr 769	Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Theorem	ad7antr 770	Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Theorem	ad7antlr 771	Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Theorem	ad8antr 772	Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)
Theorem	ad8antlr 773	Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)
Theorem	ad9antr 774	Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓)
Theorem	ad9antlr 775	Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓)
Theorem	ad10antr 776	Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓)
Theorem	ad10antlr 777	Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓)
Theorem	ad2ant2l 778	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)
Theorem	ad2ant2r 779	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)
Theorem	ad2ant2lr 780	Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)
Theorem	ad2ant2rl 781	Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒)
Theorem	adantl3r 782	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((((𝜑 ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ (((((𝜑 ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	adantl4r 783	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ (((((𝜑 ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ ((((((𝜑 ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	adantl5r 784	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((((((𝜑 ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ (((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	adantl6r 785	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ (((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ ((((((((𝜑 ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	simpll 786	Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
Theorem	simplld 787	Deduction form of simpll 786, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simplr 788	Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
Theorem	simplrd 789	Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simprl 790	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜓)
Theorem	simprld 791	Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simprr 792	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜒)
Theorem	simprrd 793	Deduction form of simprr 792, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	simplll 794	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
Theorem	simpllr 795	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
Theorem	simplrl 796	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)
Theorem	simplrr 797	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)
Theorem	simprll 798	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)
Theorem	simprlr 799	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)
Theorem	simprrl 800	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)