P. 6 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 501-600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	simplbi2com 501	A deduction eliminating a conjunct, similar to simplbi2 499. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜒 → (𝜓 → 𝜑))
Theorem	simpl2im 502	Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.) (Proof shortened by Wolf Lammen, 26-Mar-2022.)
⊢ (𝜑 → (𝜓 ∧ 𝜒))    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	simplbiim 503	Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 26-Mar-2022.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	impel 504	An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
Theorem	mpan9 505	Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → (𝜓 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	sylan9 506	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜒 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))
Theorem	sylan9r 507	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜒 → 𝜏))    ⇒   ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏))
Theorem	sylan9bb 508	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜒 ↔ 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))
Theorem	sylan9bbr 509	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜒 ↔ 𝜏))    ⇒   ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏))
Theorem	jca 510	Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). Deduction form of pm3.2 468 and pm3.2i 469. Its associated deduction is jcad 511. Equivalent to the natural deduction rule ∧ I (∧ introduction), see natded 30269. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jcad 511	Deduction conjoining the consequents of two implications. Deduction form of jca 510 and double deduction form of pm3.2 468 and pm3.2i 469. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))
Theorem	jca2 512	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))
Theorem	jca31 513	Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
Theorem	jca32 514	Join three consequents. (Contributed by FL, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))
Theorem	jcai 515	Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jcab 516	Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.)
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)))
Theorem	pm4.76 517	Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	jctil 518	Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓))
Theorem	jctir 519	Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jccir 520	Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i 30275. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by AV, 20-Aug-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jccil 521	Inference conjoining a consequent of a consequent to the left of the consequent in an implication. Remark: One can also prove this theorem using syl 17 and jca 510 (as done in jccir 520), which would be 4 bytes shorter, but one step longer than the current proof. (Proof modification is discouraged.) (Contributed by AV, 20-Aug-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓))
Theorem	jctl 522	Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
⊢ 𝜓    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜑))
Theorem	jctr 523	Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
⊢ 𝜓    ⇒   ⊢ (𝜑 → (𝜑 ∧ 𝜓))
Theorem	jctild 524	Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jctird 525	Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))
Theorem	iba 526	Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.)
⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
Theorem	ibar 527	Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
Theorem	biantru 528	A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-1993.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))
Theorem	biantrur 529	A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))
Theorem	biantrud 530	A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))
Theorem	biantrurd 531	A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
Theorem	bianfi 532	A wff conjoined with falsehood is false. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ ¬ 𝜑    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))
Theorem	bianfd 533	A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
Theorem	baib 534	Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜓 → (𝜑 ↔ 𝜒))
Theorem	baibr 535	Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜓 → (𝜒 ↔ 𝜑))
Theorem	rbaibr 536	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜒 → (𝜓 ↔ 𝜑))
Theorem	rbaib 537	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜒 → (𝜑 ↔ 𝜓))
Theorem	baibd 538	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))
Theorem	rbaibd 539	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
Theorem	bianabs 540	Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	pm5.44 541	Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) ↔ (𝜑 → (𝜓 ∧ 𝜒))))
Theorem	pm5.42 542	Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))))
Theorem	ancl 543	Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜑 ∧ 𝜓)))
Theorem	anclb 544	Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜑 ∧ 𝜓)))
Theorem	ancr 545	Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜓 ∧ 𝜑)))
Theorem	ancrb 546	Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ∧ 𝜑)))
Theorem	ancli 547	Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜑 ∧ 𝜓))
Theorem	ancri 548	Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜑))
Theorem	ancld 549	Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))
Theorem	ancrd 550	Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓)))
Theorem	impac 551	Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜓))
Theorem	anc2l 552	Conjoin antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 14-Jul-2013.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))))
Theorem	anc2r 553	Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜒 ∧ 𝜑))))
Theorem	anc2li 554	Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))
Theorem	anc2ri 555	Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜑)))
Theorem	pm4.71 556	Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓)))
Theorem	pm4.71r 557	Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 25-Jul-1999.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑)))
Theorem	pm4.71i 558	Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
Theorem	pm4.71ri 559	Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))
Theorem	pm4.71d 560	Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
Theorem	pm4.71rd 561	Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))
Theorem	pm4.24 562	Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.)
⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))
Theorem	anidm 563	Idempotent law for conjunction. (Contributed by NM, 8-Jan-2004.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)
⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
Theorem	anidmdbi 564	Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)
⊢ ((𝜑 → (𝜓 ∧ 𝜓)) ↔ (𝜑 → 𝜓))
Theorem	anidms 565	Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
⊢ ((𝜑 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	imdistan 566	Distribution of implication with conjunction. (Contributed by NM, 31-May-1999.) (Proof shortened by Wolf Lammen, 6-Dec-2012.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)))
Theorem	imdistani 567	Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))
Theorem	imdistanri 568	Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝜒 ∧ 𝜑))
Theorem	imdistand 569	Distribution of implication with conjunction (deduction form). (Contributed by NM, 27-Aug-2004.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))
Theorem	imdistanda 570	Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))
Theorem	pm5.3 571	Theorem *5.3 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)))
Theorem	pm5.32 572	Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.)
⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
Theorem	pm5.32i 573	Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))
Theorem	pm5.32ri 574	Distribution of implication over biconditional (inference form). (Contributed by NM, 12-Mar-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑))
Theorem	pm5.32d 575	Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.)
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
Theorem	pm5.32rd 576	Distribution of implication over biconditional (deduction form). (Contributed by NM, 25-Dec-2004.)
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓)))
Theorem	pm5.32da 577	Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
Theorem	sylan 578	A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	sylanb 579	A syllogism inference. (Contributed by NM, 18-May-1994.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	sylanbr 580	A syllogism inference. (Contributed by NM, 18-May-1994.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	sylanbrc 581	Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	syl2anc 582	Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	syl2anc2 583	Double syllogism inference combined with contraction. (Contributed by BTernaryTau, 29-Sep-2023.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylancl 584	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylancr 585	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝜓    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylancom 586	Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜒 ∧ 𝜓) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	sylanblc 587	Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ ((𝜓 ∧ 𝜒) ↔ 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylanblrc 588	Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	syldan 589	A syllogism deduction with conjoined antecedents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	sylbida 590	A syllogism deduction. (Contributed by SN, 16-Jul-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	sylan2 591	A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜃)
Theorem	sylan2b 592	A syllogism inference. (Contributed by NM, 21-Apr-1994.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜃)
Theorem	sylan2br 593	A syllogism inference. (Contributed by NM, 21-Apr-1994.)
⊢ (𝜒 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜃)
Theorem	syl2an 594	A double syllogism inference. For an implication-only version, see syl2im 40. (Contributed by NM, 31-Jan-1997.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜏 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
Theorem	syl2anr 595	A double syllogism inference. For an implication-only version, see syl2imc 41. (Contributed by NM, 17-Sep-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜏 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜏 ∧ 𝜑) → 𝜃)
Theorem	syl2anb 596	A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
Theorem	syl2anbr 597	A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜒 ↔ 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
Theorem	sylancb 598	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜑 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	sylancbr 599	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	syldanl 600	A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)