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