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