P. 7 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 601-700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	expl 601	Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (φ → ((ψ ∧ χ) → θ))
Theorem	impr 602	Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((φ ∧ ψ) → (χ → θ))    ⇒   ⊢ ((φ ∧ (ψ ∧ χ)) → θ)
Theorem	impl 603	Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (((φ ∧ ψ) ∧ χ) → θ)
Theorem	impac 604	Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ ((φ ∧ ψ) → (χ ∧ ψ))
Theorem	exbiri 605	Inference form of exbir 1365. This proof is exbiriVD in set.mm automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)
⊢ ((φ ∧ ψ) → (χ ↔ θ))    ⇒   ⊢ (φ → (ψ → (θ → χ)))
Theorem	simprbda 606	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
⊢ (φ → (ψ ↔ (χ ∧ θ)))    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	simplbda 607	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
⊢ (φ → (ψ ↔ (χ ∧ θ)))    ⇒   ⊢ ((φ ∧ ψ) → θ)
Theorem	simplbi2 608	Deduction eliminating a conjunct. Automatically derived from simplbi2VD in set.mm. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ (φ ↔ (ψ ∧ χ))    ⇒   ⊢ (ψ → (χ → φ))
Theorem	dfbi2 609	A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.)
⊢ ((φ ↔ ψ) ↔ ((φ → ψ) ∧ (ψ → φ)))
Theorem	dfbi 610	Definition df-bi 177 rewritten in an abbreviated form to help intuitive understanding of that definition. Note that it is a conjunction of two implications; one which asserts properties that follow from the biconditional and one which asserts properties that imply the biconditional. (Contributed by NM, 15-Aug-2008.)
⊢ (((φ ↔ ψ) → ((φ → ψ) ∧ (ψ → φ))) ∧ (((φ → ψ) ∧ (ψ → φ)) → (φ ↔ ψ)))
Theorem	pm4.71 611	Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
⊢ ((φ → ψ) ↔ (φ ↔ (φ ∧ ψ)))
Theorem	pm4.71r 612	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 613	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 614	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 615	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 616	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	pm5.32 617	Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.)
⊢ ((φ → (ψ ↔ χ)) ↔ ((φ ∧ ψ) ↔ (φ ∧ χ)))
Theorem	pm5.32i 618	Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ ((φ ∧ ψ) ↔ (φ ∧ χ))
Theorem	pm5.32ri 619	Distribution of implication over biconditional (inference rule). (Contributed by NM, 12-Mar-1995.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ ((ψ ∧ φ) ↔ (χ ∧ φ))
Theorem	pm5.32d 620	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 29-Oct-1996.)
⊢ (φ → (ψ → (χ ↔ θ)))    ⇒   ⊢ (φ → ((ψ ∧ χ) ↔ (ψ ∧ θ)))
Theorem	pm5.32rd 621	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 25-Dec-2004.)
⊢ (φ → (ψ → (χ ↔ θ)))    ⇒   ⊢ (φ → ((χ ∧ ψ) ↔ (θ ∧ ψ)))
Theorem	pm5.32da 622	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.)
⊢ ((φ ∧ ψ) → (χ ↔ θ))    ⇒   ⊢ (φ → ((ψ ∧ χ) ↔ (ψ ∧ θ)))
Theorem	biadan2 623	Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ (φ → ψ)    &   ⊢ (ψ → (φ ↔ χ))    ⇒   ⊢ (φ ↔ (ψ ∧ χ))
Theorem	pm4.24 624	Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
⊢ (φ ↔ (φ ∧ φ))
Theorem	anidm 625	Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)
⊢ ((φ ∧ φ) ↔ φ)
Theorem	anidms 626	Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
⊢ ((φ ∧ φ) → ψ)    ⇒   ⊢ (φ → ψ)
Theorem	anidmdbi 627	Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)
⊢ ((φ → (ψ ∧ ψ)) ↔ (φ → ψ))
Theorem	anasss 628	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ χ)) → θ)
Theorem	anassrs 629	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ (((φ ∧ ψ) ∧ χ) → θ)
Theorem	anass 630	Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (((φ ∧ ψ) ∧ χ) ↔ (φ ∧ (ψ ∧ χ)))
Theorem	sylanl1 631	A syllogism inference. (Contributed by NM, 10-Mar-2005.)
⊢ (φ → ψ)    &   ⊢ (((ψ ∧ χ) ∧ θ) → τ)    ⇒   ⊢ (((φ ∧ χ) ∧ θ) → τ)
Theorem	sylanl2 632	A syllogism inference. (Contributed by NM, 1-Jan-2005.)
⊢ (φ → χ)    &   ⊢ (((ψ ∧ χ) ∧ θ) → τ)    ⇒   ⊢ (((ψ ∧ φ) ∧ θ) → τ)
Theorem	sylanr1 633	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
⊢ (φ → χ)    &   ⊢ ((ψ ∧ (χ ∧ θ)) → τ)    ⇒   ⊢ ((ψ ∧ (φ ∧ θ)) → τ)
Theorem	sylanr2 634	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
⊢ (φ → θ)    &   ⊢ ((ψ ∧ (χ ∧ θ)) → τ)    ⇒   ⊢ ((ψ ∧ (χ ∧ φ)) → τ)
Theorem	sylani 635	A syllogism inference. (Contributed by NM, 2-May-1996.)
⊢ (φ → χ)    &   ⊢ (ψ → ((χ ∧ θ) → τ))    ⇒   ⊢ (ψ → ((φ ∧ θ) → τ))
Theorem	sylan2i 636	A syllogism inference. (Contributed by NM, 1-Aug-1994.)
⊢ (φ → θ)    &   ⊢ (ψ → ((χ ∧ θ) → τ))    ⇒   ⊢ (ψ → ((χ ∧ φ) → τ))
Theorem	syl2ani 637	A syllogism inference. (Contributed by NM, 3-Aug-1999.)
⊢ (φ → χ)    &   ⊢ (η → θ)    &   ⊢ (ψ → ((χ ∧ θ) → τ))    ⇒   ⊢ (ψ → ((φ ∧ η) → τ))
Theorem	sylan9 638	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (χ → τ))    ⇒   ⊢ ((φ ∧ θ) → (ψ → τ))
Theorem	sylan9r 639	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (χ → τ))    ⇒   ⊢ ((θ ∧ φ) → (ψ → τ))
Theorem	mtand 640	A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
⊢ (φ → ¬ χ)    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mtord 641	A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (φ → ¬ χ)    &   ⊢ (φ → ¬ θ)    &   ⊢ (φ → (ψ → (χ ∨ θ)))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	syl2anc 642	Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ ((ψ ∧ χ) → θ)    ⇒   ⊢ (φ → θ)
Theorem	sylancl 643	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (φ → ψ)    &   ⊢ χ    &   ⊢ ((ψ ∧ χ) → θ)    ⇒   ⊢ (φ → θ)
Theorem	sylancr 644	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ψ    &   ⊢ (φ → χ)    &   ⊢ ((ψ ∧ χ) → θ)    ⇒   ⊢ (φ → θ)
Theorem	sylanbrc 645	Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (θ ↔ (ψ ∧ χ))    ⇒   ⊢ (φ → θ)
Theorem	sylancb 646	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
⊢ (φ ↔ ψ)    &   ⊢ (φ ↔ χ)    &   ⊢ ((ψ ∧ χ) → θ)    ⇒   ⊢ (φ → θ)
Theorem	sylancbr 647	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
⊢ (ψ ↔ φ)    &   ⊢ (χ ↔ φ)    &   ⊢ ((ψ ∧ χ) → θ)    ⇒   ⊢ (φ → θ)
Theorem	sylancom 648	Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((χ ∧ ψ) → θ)    ⇒   ⊢ ((φ ∧ ψ) → θ)
Theorem	mpdan 649	An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
⊢ (φ → ψ)    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (φ → χ)
Theorem	mpancom 650	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	mpan 651	An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ φ    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (ψ → χ)
Theorem	mpan2 652	An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ ψ    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (φ → χ)
Theorem	mp2an 653	An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
⊢ φ    &   ⊢ ψ    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ χ
Theorem	mp4an 654	An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ φ    &   ⊢ ψ    &   ⊢ χ    &   ⊢ θ    &   ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) → τ)    ⇒   ⊢ τ
Theorem	mpan2d 655	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ (φ → χ)    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	mpand 656	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ (φ → ψ)    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → (χ → θ))
Theorem	mpani 657	An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ ψ    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → (χ → θ))
Theorem	mpan2i 658	An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ χ    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	mp2ani 659	An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ ψ    &   ⊢ χ    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → θ)
Theorem	mp2and 660	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → θ)
Theorem	mpanl1 661	An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ φ    &   ⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ ((ψ ∧ χ) → θ)
Theorem	mpanl2 662	An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ ψ    &   ⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ χ) → θ)
Theorem	mpanl12 663	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
⊢ φ    &   ⊢ ψ    &   ⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (χ → θ)
Theorem	mpanr1 664	An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ ψ    &   ⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ χ) → θ)
Theorem	mpanr2 665	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 666	An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
⊢ ψ    &   ⊢ χ    &   ⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ (φ → θ)
Theorem	mpanlr1 667	An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ ψ    &   ⊢ (((φ ∧ (ψ ∧ χ)) ∧ θ) → τ)    ⇒   ⊢ (((φ ∧ χ) ∧ θ) → τ)
Theorem	pm5.74da 668	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 4-May-2007.)
⊢ ((φ ∧ ψ) → (χ ↔ θ))    ⇒   ⊢ (φ → ((ψ → χ) ↔ (ψ → θ)))
Theorem	pm4.45 669	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (φ ↔ (φ ∧ (φ ∨ ψ)))
Theorem	imdistan 670	Distribution of implication with conjunction. (Contributed by NM, 31-May-1999.) (Proof shortened by Wolf Lammen, 6-Dec-2012.)
⊢ ((φ → (ψ → χ)) ↔ ((φ ∧ ψ) → (φ ∧ χ)))
Theorem	imdistani 671	Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ ((φ ∧ ψ) → (φ ∧ χ))
Theorem	imdistanri 672	Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ ((ψ ∧ φ) → (χ ∧ φ))
Theorem	imdistand 673	Distribution of implication with conjunction (deduction rule). (Contributed by NM, 27-Aug-2004.)
⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ (φ → ((ψ ∧ χ) → (ψ ∧ θ)))
Theorem	imdistanda 674	Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((φ ∧ ψ) → (χ → θ))    ⇒   ⊢ (φ → ((ψ ∧ χ) → (ψ ∧ θ)))
Theorem	anbi2i 675	Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ((χ ∧ φ) ↔ (χ ∧ ψ))
Theorem	anbi1i 676	Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ((φ ∧ χ) ↔ (ψ ∧ χ))
Theorem	anbi2ci 677	Variant of anbi2i 675 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ((φ ∧ χ) ↔ (χ ∧ ψ))
Theorem	anbi12i 678	Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ θ)    ⇒   ⊢ ((φ ∧ χ) ↔ (ψ ∧ θ))
Theorem	anbi12ci 679	Variant of anbi12i 678 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ θ)    ⇒   ⊢ ((φ ∧ χ) ↔ (θ ∧ ψ))
Theorem	sylan9bb 680	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (χ ↔ τ))    ⇒   ⊢ ((φ ∧ θ) → (ψ ↔ τ))
Theorem	sylan9bbr 681	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (χ ↔ τ))    ⇒   ⊢ ((θ ∧ φ) → (ψ ↔ τ))
Theorem	orbi2d 682	Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((θ ∨ ψ) ↔ (θ ∨ χ)))
Theorem	orbi1d 683	Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((ψ ∨ θ) ↔ (χ ∨ θ)))
Theorem	anbi2d 684	Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((θ ∧ ψ) ↔ (θ ∧ χ)))
Theorem	anbi1d 685	Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((ψ ∧ θ) ↔ (χ ∧ θ)))
Theorem	orbi1 686	Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ ↔ ψ) → ((φ ∨ χ) ↔ (ψ ∨ χ)))
Theorem	anbi1 687	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 688	Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 16-Nov-2013.)
⊢ ((φ ↔ ψ) → ((χ ∧ φ) ↔ (χ ∧ ψ)))
Theorem	bitr 689	Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ ↔ ψ) ∧ (ψ ↔ χ)) → (φ ↔ χ))
Theorem	orbi12d 690	Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → ((ψ ∨ θ) ↔ (χ ∨ τ)))
Theorem	anbi12d 691	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → ((ψ ∧ θ) ↔ (χ ∧ τ)))
Theorem	pm5.3 692	Theorem *5.3 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (((φ ∧ ψ) → χ) ↔ ((φ ∧ ψ) → (φ ∧ χ)))
Theorem	pm5.61 693	Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
⊢ (((φ ∨ ψ) ∧ ¬ ψ) ↔ (φ ∧ ¬ ψ))
Theorem	adantll 694	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (((θ ∧ φ) ∧ ψ) → χ)
Theorem	adantlr 695	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (((φ ∧ θ) ∧ ψ) → χ)
Theorem	adantrl 696	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ ((φ ∧ (θ ∧ ψ)) → χ)
Theorem	adantrr 697	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ ((φ ∧ (ψ ∧ θ)) → χ)
Theorem	adantlll 698	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ ((((τ ∧ φ) ∧ ψ) ∧ χ) → θ)
Theorem	adantllr 699	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ ((((φ ∧ τ) ∧ ψ) ∧ χ) → θ)
Theorem	adantlrl 700	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (((φ ∧ (τ ∧ ψ)) ∧ χ) → θ)