P. 7 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 601-700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sylan2i 601	A syllogism inference. (Contributed by NM, 1-Aug-1994.)
⊢ (𝜑 → 𝜃)    &   ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜓 → ((𝜒 ∧ 𝜑) → 𝜏))
Theorem	syl2ani 602	A syllogism inference. (Contributed by NM, 3-Aug-1999.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜂 → 𝜃)    &   ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜓 → ((𝜑 ∧ 𝜂) → 𝜏))
Theorem	syl2and 603	A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))
Theorem	anim12d 604	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
Theorem	anim12d1 605	Variant of anim12d 604 where the second implication does not depend on the antecedent. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
Theorem	anim1d 606	Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))
Theorem	anim2d 607	Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))
Theorem	anim12i 608	Conjoin antecedents and consequents of two premises. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))
Theorem	anim12ci 609	Variant of anim12i 608 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓))
Theorem	anim1i 610	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
Theorem	anim1ci 611	Introduce conjunct to both sides of an implication. (Contributed by Peter Mazsa, 24-Sep-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜒 ∧ 𝜓))
Theorem	anim2i 612	Introduce conjunct to both sides of an implication. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))
Theorem	anim12ii 613	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜓 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → (𝜒 ∧ 𝜏)))
Theorem	anim12dan 614	Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏))
Theorem	im2anan9 615	Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂)))
Theorem	im2anan9r 616	Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂)))
Theorem	pm3.45 617	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒)))
Theorem	anbi2i 618	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 619	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 620	Variant of anbi2i 618 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
Theorem	anbi1ci 621	Variant of anbi1i 619 with commutation. (Contributed by Peter Mazsa, 7-Mar-2020.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜓 ∧ 𝜒))
Theorem	anbi12i 622	Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
Theorem	anbi12ci 623	Variant of anbi12i 622 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))
Theorem	anbi2d 624	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 625	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	anbi12d 626	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
Theorem	anbi1 627	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 628	Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 16-Nov-2013.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓)))
Theorem	anbi1cd 629	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	pm4.38 630	Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ↔ 𝜒) ∧ (𝜓 ↔ 𝜃)) → ((𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃)))
Theorem	bi2anan9 631	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜏 ↔ 𝜂))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
Theorem	bi2anan9r 632	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜏 ↔ 𝜂))    ⇒   ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
Theorem	bi2bian9 633	Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜏 ↔ 𝜂))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ↔ 𝜏) ↔ (𝜒 ↔ 𝜂)))
Theorem	bianass 634	An inference to merge two lists of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜂 ∧ 𝜑) ↔ ((𝜂 ∧ 𝜓) ∧ 𝜒))
Theorem	bianassc 635	An inference to merge two lists of conjuncts. (Contributed by Peter Mazsa, 24-Sep-2022.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜂 ∧ 𝜑) ↔ ((𝜓 ∧ 𝜂) ∧ 𝜒))
Theorem	an21 636	Swap two conjuncts. (Contributed by Peter Mazsa, 18-Sep-2022.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
Theorem	an12 637	Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Peter Mazsa, 18-Sep-2022.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
Theorem	an32 638	A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	an13 639	A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜑)))
Theorem	an31 640	A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑))
Theorem	an12s 641	Swap two conjuncts in antecedent. The label suffix "s" means that an12 637 is combined with syl 17 (or a variant). (Contributed by NM, 13-Mar-1996.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃)
Theorem	ancom2s 642	Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)
Theorem	an13s 643	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑)) → 𝜃)
Theorem	an32s 644	Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)
Theorem	ancom1s 645	Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃)
Theorem	an31s 646	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜒 ∧ 𝜓) ∧ 𝜑) → 𝜃)
Theorem	anass1rs 647	Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)
Theorem	an4 648	Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
Theorem	an42 649	Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)))
Theorem	an43 650	Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜒)))
Theorem	an3 651	A rearrangement of conjuncts. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → (𝜑 ∧ 𝜃))
Theorem	an4s 652	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)
Theorem	an42s 653	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏)
Theorem	anabs1 654	Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) ↔ (𝜑 ∧ 𝜓))
Theorem	anabs5 655	Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓))
Theorem	anabs7 656	Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 17-Nov-2013.)
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓))
Theorem	anabsan 657	Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996.)
⊢ (((𝜑 ∧ 𝜑) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabss1 658	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabss4 659	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabss5 660	Absorption of antecedent into conjunction. (Contributed by NM, 10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabsi5 661	Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabsi6 662	Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
⊢ (𝜑 → ((𝜓 ∧ 𝜑) → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabsi7 663	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabsi8 664	Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)
⊢ (𝜓 → ((𝜓 ∧ 𝜑) → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabss7 665	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.)
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabsan2 666	Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabss3 667	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anandi 668	Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
Theorem	anandir 669	Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)))
Theorem	anandis 670	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)
Theorem	anandirs 671	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏)
Theorem	sylanl1 672	A syllogism inference. (Contributed by NM, 10-Mar-2005.)
⊢ (𝜑 → 𝜓)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	sylanl2 673	A syllogism inference. (Contributed by NM, 1-Jan-2005.)
⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏)
Theorem	sylanr1 674	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜃)) → 𝜏)
Theorem	sylanr2 675	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜑)) → 𝜏)
Theorem	syl6an 676	A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜒 → 𝜏))
Theorem	syl2an2r 677	syl2anr 592 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Mar-2022.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜏)
Theorem	syl2an2rOLD 678	Obsolete proof of syl2an2r 677 as of 28-Mar-2022. (Contributed by Alan Sare, 27-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜏)
Theorem	syl2an2 679	syl2an 591 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜒 ∧ 𝜑) → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜒 ∧ 𝜑) → 𝜏)
Theorem	mpdan 680	An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mpancom 681	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 682	A deduction which "stacks" a hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.) (Proof shortened by Wolf Lammen, 28-Mar-2021.)
⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mpan 683	An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜑    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	mpan2 684	An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mp2an 685	An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	mp4an 686	An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ 𝜏
Theorem	mpan2d 687	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	mpand 688	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜃))
Theorem	mpani 689	An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ 𝜓    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜃))
Theorem	mpan2i 690	An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ 𝜒    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	mp2ani 691	An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mp2and 692	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mpanl1 693	An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜑    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	mpanl2 694	An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 𝜓    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	mpanl12 695	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	mpanr1 696	An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	mpanr2 697	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 698	An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mpanlr1 699	An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ 𝜓    &   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	mpbirand 700	Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))