P. 5 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 401-500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sylanl2 401	A syllogism inference. (Contributed by NM, 1-Jan-2005.)
⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏)
Theorem	sylanr1 402	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜃)) → 𝜏)
Theorem	sylanr2 403	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜑)) → 𝜏)
Theorem	sylani 404	A syllogism inference. (Contributed by NM, 2-May-1996.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜓 → ((𝜑 ∧ 𝜃) → 𝜏))
Theorem	sylan2i 405	A syllogism inference. (Contributed by NM, 1-Aug-1994.)
⊢ (𝜑 → 𝜃)    &   ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜓 → ((𝜒 ∧ 𝜑) → 𝜏))
Theorem	syl2ani 406	A syllogism inference. (Contributed by NM, 3-Aug-1999.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜂 → 𝜃)    &   ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜓 → ((𝜑 ∧ 𝜂) → 𝜏))
Theorem	sylan9 407	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜒 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))
Theorem	sylan9r 408	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜒 → 𝜏))    ⇒   ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏))
Theorem	syl2anc 409	Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	syl2anc2 410	Double syllogism inference combined with contraction. (Contributed by BTernaryTau, 29-Sep-2023.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylancl 411	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylancr 412	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝜓    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylanblc 413	Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ ((𝜓 ∧ 𝜒) ↔ 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylanblrc 414	Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylanbrc 415	Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylancb 416	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜑 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylancbr 417	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylancom 418	Syllogism inference with commutation of antecents. (Contributed by NM, 2-Jul-2008.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜒 ∧ 𝜓) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mpdan 419	An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mpancom 420	An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ (𝜓 → 𝜑)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	mpidan 421	A deduction which "stacks" a hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.) (Proof shortened by Wolf Lammen, 28-Mar-2021.)
⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mpan 422	An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜑    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	mpan2 423	An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mp2an 424	An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	mp4an 425	An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2011.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ 𝜏
Theorem	mpan2d 426	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	mpand 427	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜃))
Theorem	mpani 428	An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ 𝜓    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜃))
Theorem	mpan2i 429	An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ 𝜒    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	mp2ani 430	An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mp2and 431	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mpanl1 432	An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜑    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	mpanl2 433	An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 𝜓    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	mpanl12 434	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	mpanr1 435	An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	mpanr2 436	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 437	An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mpanlr1 438	An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜓    &   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	mpbirand 439	Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	mpbiran2d 440	Detach truth from conjunction in biconditional. Deduction form. (Contributed by Peter Mazsa, 24-Sep-2022.)
⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	pm5.74da 441	Distribution of implication over biconditional (deduction form). (Contributed by NM, 4-May-2007.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
Theorem	imdistan 442	Distribution of implication with conjunction. (Contributed by NM, 31-May-1999.) (Proof shortened by Wolf Lammen, 6-Dec-2012.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)))
Theorem	imdistani 443	Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))
Theorem	imdistanri 444	Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝜒 ∧ 𝜑))
Theorem	imdistand 445	Distribution of implication with conjunction (deduction form). (Contributed by NM, 27-Aug-2004.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))
Theorem	imdistanda 446	Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))
Theorem	pm5.32d 447	Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.) (Revised by NM, 31-Jan-2015.)
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
Theorem	pm5.32rd 448	Distribution of implication over biconditional (deduction form). (Contributed by NM, 25-Dec-2004.)
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓)))
Theorem	pm5.32da 449	Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
Theorem	pm5.32 450	Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.) (Revised by NM, 31-Jan-2015.)
⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
Theorem	pm5.32i 451	Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))
Theorem	pm5.32ri 452	Distribution of implication over biconditional (inference form). (Contributed by NM, 12-Mar-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑))
Theorem	biadan2 453	Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
Theorem	anbi2i 454	Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))
Theorem	anbi1i 455	Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
Theorem	anbi2ci 456	Variant of anbi2i 454 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
Theorem	anbi12i 457	Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
Theorem	anbi12ci 458	Variant of anbi12i 457 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))
Theorem	sylan9bb 459	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜒 ↔ 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))
Theorem	sylan9bbr 460	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜒 ↔ 𝜏))    ⇒   ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏))
Theorem	anbi2d 461	Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒)))
Theorem	anbi1d 462	Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))
Theorem	anbi1 463	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 464	Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 16-Nov-2013.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓)))
Theorem	anbi1cd 465	Introduce a proposition as left conjunct on the left-hand side and right conjunct on the right-hand side of an equivalence. Deduction form. (Contributed by Peter Mazsa, 22-May-2021.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃)))
Theorem	bianass 466	An inference to merge two lists of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜂 ∧ 𝜑) ↔ ((𝜂 ∧ 𝜓) ∧ 𝜒))
Theorem	bianassc 467	An inference to merge two lists of conjuncts. (Contributed by Peter Mazsa, 24-Sep-2022.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜂 ∧ 𝜑) ↔ ((𝜓 ∧ 𝜂) ∧ 𝜒))
Theorem	an21 468	Swap two conjuncts. (Contributed by Peter Mazsa, 18-Sep-2022.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
Theorem	bitr 469	Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜓 ↔ 𝜒)) → (𝜑 ↔ 𝜒))
Theorem	anbi12d 470	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
Theorem	mpan10 471	Modus ponens mixed with several conjunctions. (Contributed by Jim Kingdon, 7-Jan-2018.)
⊢ ((((𝜑 → 𝜓) ∧ 𝜒) ∧ 𝜑) → (𝜓 ∧ 𝜒))
Theorem	pm5.3 472	Theorem *5.3 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)))
Theorem	adantll 473	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)
Theorem	adantlr 474	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
Theorem	adantrl 475	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)
Theorem	adantrr 476	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)
Theorem	adantlll 477	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	adantllr 478	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	adantlrl 479	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)
Theorem	adantlrr 480	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)
Theorem	adantrll 481	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ ((𝜏 ∧ 𝜓) ∧ 𝜒)) → 𝜃)
Theorem	adantrlr 482	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜏) ∧ 𝜒)) → 𝜃)
Theorem	adantrrl 483	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜏 ∧ 𝜒))) → 𝜃)
Theorem	adantrrr 484	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜏))) → 𝜃)
Theorem	ad2antrr 485	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)
Theorem	ad2antlr 486	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)
Theorem	ad2antrl 487	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)
Theorem	ad2antll 488	Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)
Theorem	ad3antrrr 489	Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Theorem	ad3antlr 490	Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Theorem	ad4antr 491	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Theorem	ad4antlr 492	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Theorem	ad5antr 493	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Theorem	ad5antlr 494	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Theorem	ad6antr 495	Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Theorem	ad6antlr 496	Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Theorem	ad7antr 497	Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Theorem	ad7antlr 498	Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Theorem	ad8antr 499	Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)
Theorem	ad8antlr 500	Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)