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