P. 9 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 801-900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	anandi 801	Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
⊢ ((φ ∧ (ψ ∧ χ)) ↔ ((φ ∧ ψ) ∧ (φ ∧ χ)))
Theorem	anandir 802	Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
⊢ (((φ ∧ ψ) ∧ χ) ↔ ((φ ∧ χ) ∧ (ψ ∧ χ)))
Theorem	anandis 803	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
⊢ (((φ ∧ ψ) ∧ (φ ∧ χ)) → τ)    ⇒   ⊢ ((φ ∧ (ψ ∧ χ)) → τ)
Theorem	anandirs 804	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
⊢ (((φ ∧ χ) ∧ (ψ ∧ χ)) → τ)    ⇒   ⊢ (((φ ∧ ψ) ∧ χ) → τ)
Theorem	impbida 805	Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((φ ∧ χ) → ψ)    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	pm3.48 806	Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.)
⊢ (((φ → ψ) ∧ (χ → θ)) → ((φ ∨ χ) → (ψ ∨ θ)))
Theorem	pm3.45 807	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ → ψ) → ((φ ∧ χ) → (ψ ∧ χ)))
Theorem	im2anan9 808	Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (τ → η))    ⇒   ⊢ ((φ ∧ θ) → ((ψ ∧ τ) → (χ ∧ η)))
Theorem	im2anan9r 809	Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (τ → η))    ⇒   ⊢ ((θ ∧ φ) → ((ψ ∧ τ) → (χ ∧ η)))
Theorem	anim12dan 810	Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((φ ∧ θ) → τ)    ⇒   ⊢ ((φ ∧ (ψ ∧ θ)) → (χ ∧ τ))
Theorem	orim12d 811	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (θ → τ))    ⇒   ⊢ (φ → ((ψ ∨ θ) → (χ ∨ τ)))
Theorem	orim1d 812	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ((ψ ∨ θ) → (χ ∨ θ)))
Theorem	orim2d 813	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ((θ ∨ ψ) → (θ ∨ χ)))
Theorem	orim2 814	Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)
⊢ ((ψ → χ) → ((φ ∨ ψ) → (φ ∨ χ)))
Theorem	pm2.38 815	Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((ψ → χ) → ((ψ ∨ φ) → (χ ∨ φ)))
Theorem	pm2.36 816	Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((ψ → χ) → ((φ ∨ ψ) → (χ ∨ φ)))
Theorem	pm2.37 817	Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((ψ → χ) → ((ψ ∨ φ) → (φ ∨ χ)))
Theorem	pm2.73 818	Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ → ψ) → (((φ ∨ ψ) ∨ χ) → (ψ ∨ χ)))
Theorem	pm2.74 819	Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ ((ψ → φ) → (((φ ∨ ψ) ∨ χ) → (φ ∨ χ)))
Theorem	orimdi 820	Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.)
⊢ ((φ ∨ (ψ → χ)) ↔ ((φ ∨ ψ) → (φ ∨ χ)))
Theorem	pm2.76 821	Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ ∨ (ψ → χ)) → ((φ ∨ ψ) → (φ ∨ χ)))
Theorem	pm2.75 822	Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.)
⊢ ((φ ∨ ψ) → ((φ ∨ (ψ → χ)) → (φ ∨ χ)))
Theorem	pm2.8 823	Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
⊢ ((φ ∨ ψ) → ((¬ ψ ∨ χ) → (φ ∨ χ)))
Theorem	pm2.81 824	Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ ((ψ → (χ → θ)) → ((φ ∨ ψ) → ((φ ∨ χ) → (φ ∨ θ))))
Theorem	pm2.82 825	Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ ∨ ψ) ∨ χ) → (((φ ∨ ¬ χ) ∨ θ) → ((φ ∨ ψ) ∨ θ)))
Theorem	pm2.85 826	Theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
⊢ (((φ ∨ ψ) → (φ ∨ χ)) → (φ ∨ (ψ → χ)))
Theorem	pm3.2ni 827	Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)
⊢ ¬ φ    &   ⊢ ¬ ψ    ⇒   ⊢ ¬ (φ ∨ ψ)
Theorem	orabs 828	Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Feb-2014.)
⊢ (φ ↔ ((φ ∨ ψ) ∧ φ))
Theorem	oranabs 829	Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.)
⊢ (((φ ∨ ¬ ψ) ∧ ψ) ↔ (φ ∧ ψ))
Theorem	pm5.1 830	Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123. (Contributed by NM, 21-May-1994.)
⊢ ((φ ∧ ψ) → (φ ↔ ψ))
Theorem	pm5.21 831	Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124. (Contributed by NM, 21-May-1994.)
⊢ ((¬ φ ∧ ¬ ψ) → (φ ↔ ψ))
Theorem	pm3.43 832	Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ → ψ) ∧ (φ → χ)) → (φ → (ψ ∧ χ)))
Theorem	jcab 833	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	ordi 834	Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 28-Nov-2013.)
⊢ ((φ ∨ (ψ ∧ χ)) ↔ ((φ ∨ ψ) ∧ (φ ∨ χ)))
Theorem	ordir 835	Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((φ ∧ ψ) ∨ χ) ↔ ((φ ∨ χ) ∧ (ψ ∨ χ)))
Theorem	pm4.76 836	Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ → ψ) ∧ (φ → χ)) ↔ (φ → (ψ ∧ χ)))
Theorem	andi 837	Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
⊢ ((φ ∧ (ψ ∨ χ)) ↔ ((φ ∧ ψ) ∨ (φ ∧ χ)))
Theorem	andir 838	Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((φ ∨ ψ) ∧ χ) ↔ ((φ ∧ χ) ∨ (ψ ∧ χ)))
Theorem	orddi 839	Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((φ ∧ ψ) ∨ (χ ∧ θ)) ↔ (((φ ∨ χ) ∧ (φ ∨ θ)) ∧ ((ψ ∨ χ) ∧ (ψ ∨ θ))))
Theorem	anddi 840	Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((φ ∨ ψ) ∧ (χ ∨ θ)) ↔ (((φ ∧ χ) ∨ (φ ∧ θ)) ∨ ((ψ ∧ χ) ∨ (ψ ∧ θ))))
Theorem	pm4.39 841	Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ ↔ χ) ∧ (ψ ↔ θ)) → ((φ ∨ ψ) ↔ (χ ∨ θ)))
Theorem	pm4.38 842	Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ ↔ χ) ∧ (ψ ↔ θ)) → ((φ ∧ ψ) ↔ (χ ∧ θ)))
Theorem	bi2anan9 843	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (τ ↔ η))    ⇒   ⊢ ((φ ∧ θ) → ((ψ ∧ τ) ↔ (χ ∧ η)))
Theorem	bi2anan9r 844	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (τ ↔ η))    ⇒   ⊢ ((θ ∧ φ) → ((ψ ∧ τ) ↔ (χ ∧ η)))
Theorem	bi2bian9 845	Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (τ ↔ η))    ⇒   ⊢ ((φ ∧ θ) → ((ψ ↔ τ) ↔ (χ ↔ η)))
Theorem	pm4.72 846	Implication in terms of biconditional and disjunction. Theorem *4.72 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jan-2013.)
⊢ ((φ → ψ) ↔ (ψ ↔ (φ ∨ ψ)))
Theorem	imimorb 847	Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
⊢ (((ψ → χ) → (φ → χ)) ↔ (φ → (ψ ∨ χ)))
Theorem	pm5.33 848	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ ∧ (ψ → χ)) ↔ (φ ∧ ((φ ∧ ψ) → χ)))
Theorem	pm5.36 849	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ ∧ (φ ↔ ψ)) ↔ (ψ ∧ (φ ↔ ψ)))
Theorem	bianabs 850	Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)
⊢ (φ → (ψ ↔ (φ ∧ χ)))    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	oibabs 851	Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
⊢ (((φ ∨ ψ) → (φ ↔ ψ)) ↔ (φ ↔ ψ))
Theorem	pm3.24 852	Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ¬ (φ ∧ ¬ φ)
Theorem	pm2.26 853	Theorem *2.26 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
⊢ (¬ φ ∨ ((φ → ψ) → ψ))
Theorem	pm5.11 854	Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ → ψ) ∨ (¬ φ → ψ))
Theorem	pm5.12 855	Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ → ψ) ∨ (φ → ¬ ψ))
Theorem	pm5.14 856	Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ → ψ) ∨ (ψ → χ))
Theorem	pm5.13 857	Theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ ((φ → ψ) ∨ (ψ → φ))
Theorem	pm5.17 858	Theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Jan-2013.)
⊢ (((φ ∨ ψ) ∧ ¬ (φ ∧ ψ)) ↔ (φ ↔ ¬ ψ))
Theorem	pm5.15 859	Theorem *5.15 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 15-Oct-2013.)
⊢ ((φ ↔ ψ) ∨ (φ ↔ ¬ ψ))
Theorem	pm5.16 860	Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 17-Oct-2013.)
⊢ ¬ ((φ ↔ ψ) ∧ (φ ↔ ¬ ψ))
Theorem	xor 861	Two ways to express "exclusive or." Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.)
⊢ (¬ (φ ↔ ψ) ↔ ((φ ∧ ¬ ψ) ∨ (ψ ∧ ¬ φ)))
Theorem	nbi2 862	Two ways to express "exclusive or." (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
⊢ (¬ (φ ↔ ψ) ↔ ((φ ∨ ψ) ∧ ¬ (φ ∧ ψ)))
Theorem	dfbi3 863	An alternate definition of the biconditional. Theorem *5.23 of [WhiteheadRussell] p. 124. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
⊢ ((φ ↔ ψ) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)))
Theorem	pm5.24 864	Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ ((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)) ↔ ((φ ∧ ¬ ψ) ∨ (ψ ∧ ¬ φ)))
Theorem	xordi 865	Conjunction distributes over exclusive-or, using ¬ (φ ↔ ψ) to express exclusive-or. This is one way to interpret the distributive law of multiplication over addition in modulo 2 arithmetic. (Contributed by NM, 3-Oct-2008.)
⊢ ((φ ∧ ¬ (ψ ↔ χ)) ↔ ¬ ((φ ∧ ψ) ↔ (φ ∧ χ)))
Theorem	biort 866	A wff disjoined with truth is true. (Contributed by NM, 23-May-1999.)
⊢ (φ → (φ ↔ (φ ∨ ψ)))
Theorem	pm5.55 867	Theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)
⊢ (((φ ∨ ψ) ↔ φ) ∨ ((φ ∨ ψ) ↔ ψ))
1.2.7  Miscellaneous theorems of propositional calculus
Theorem	pm5.21nd 868	Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)
⊢ ((φ ∧ ψ) → θ)    &   ⊢ ((φ ∧ χ) → θ)    &   ⊢ (θ → (ψ ↔ χ))    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	pm5.35 869	Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ → ψ) ∧ (φ → χ)) → (φ → (ψ ↔ χ)))
Theorem	pm5.54 870	Theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 7-Nov-2013.)
⊢ (((φ ∧ ψ) ↔ φ) ∨ ((φ ∧ ψ) ↔ ψ))
Theorem	baib 871	Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
⊢ (φ ↔ (ψ ∧ χ))    ⇒   ⊢ (ψ → (φ ↔ χ))
Theorem	baibr 872	Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
⊢ (φ ↔ (ψ ∧ χ))    ⇒   ⊢ (ψ → (χ ↔ φ))
Theorem	rbaib 873	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (φ ↔ (ψ ∧ χ))    ⇒   ⊢ (χ → (φ ↔ ψ))
Theorem	rbaibr 874	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (φ ↔ (ψ ∧ χ))    ⇒   ⊢ (χ → (ψ ↔ φ))
Theorem	baibd 875	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (φ → (ψ ↔ (χ ∧ θ)))    ⇒   ⊢ ((φ ∧ χ) → (ψ ↔ θ))
Theorem	rbaibd 876	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (φ → (ψ ↔ (χ ∧ θ)))    ⇒   ⊢ ((φ ∧ θ) → (ψ ↔ χ))
Theorem	pm5.44 877	Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ → ψ) → ((φ → χ) ↔ (φ → (ψ ∧ χ))))
Theorem	pm5.6 878	Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.)
⊢ (((φ ∧ ¬ ψ) → χ) ↔ (φ → (ψ ∨ χ)))
Theorem	orcanai 879	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
⊢ (φ → (ψ ∨ χ))    ⇒   ⊢ ((φ ∧ ¬ ψ) → χ)
Theorem	intnan 880	Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
⊢ ¬ φ    ⇒   ⊢ ¬ (ψ ∧ φ)
Theorem	intnanr 881	Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
⊢ ¬ φ    ⇒   ⊢ ¬ (φ ∧ ψ)
Theorem	intnand 882	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
⊢ (φ → ¬ ψ)    ⇒   ⊢ (φ → ¬ (χ ∧ ψ))
Theorem	intnanrd 883	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
⊢ (φ → ¬ ψ)    ⇒   ⊢ (φ → ¬ (ψ ∧ χ))
Theorem	mpbiran 884	Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)
⊢ ψ    &   ⊢ (φ ↔ (ψ ∧ χ))    ⇒   ⊢ (φ ↔ χ)
Theorem	mpbiran2 885	Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)
⊢ χ    &   ⊢ (φ ↔ (ψ ∧ χ))    ⇒   ⊢ (φ ↔ ψ)
Theorem	mpbir2an 886	Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
⊢ ψ    &   ⊢ χ    &   ⊢ (φ ↔ (ψ ∧ χ))    ⇒   ⊢ φ
Theorem	mpbi2and 887	Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → ((ψ ∧ χ) ↔ θ))    ⇒   ⊢ (φ → θ)
Theorem	mpbir2and 888	Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → (ψ ↔ (χ ∧ θ)))    ⇒   ⊢ (φ → ψ)
Theorem	pm5.62 889	Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)
⊢ (((φ ∧ ψ) ∨ ¬ ψ) ↔ (φ ∨ ¬ ψ))
Theorem	pm5.63 890	Theorem *5.63 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
⊢ ((φ ∨ ψ) ↔ (φ ∨ (¬ φ ∧ ψ)))
Theorem	bianfi 891	A wff conjoined with falsehood is false. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ ¬ φ    ⇒   ⊢ (φ ↔ (ψ ∧ φ))
Theorem	bianfd 892	A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
⊢ (φ → ¬ ψ)    ⇒   ⊢ (φ → (ψ ↔ (ψ ∧ χ)))
Theorem	pm4.43 893	Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ (φ ↔ ((φ ∨ ψ) ∧ (φ ∨ ¬ ψ)))
Theorem	pm4.82 894	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ → ψ) ∧ (φ → ¬ ψ)) ↔ ¬ φ)
Theorem	pm4.83 895	Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ → ψ) ∧ (¬ φ → ψ)) ↔ ψ)
Theorem	pclem6 896	Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.)
⊢ ((φ ↔ (ψ ∧ ¬ φ)) → ¬ ψ)
Theorem	biantr 897	A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)
⊢ (((φ ↔ ψ) ∧ (χ ↔ ψ)) → (φ ↔ χ))
Theorem	orbidi 898	Disjunction distributes over the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384. (Contributed by NM, 8-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Feb-2013.)
⊢ ((φ ∨ (ψ ↔ χ)) ↔ ((φ ∨ ψ) ↔ (φ ∨ χ)))
Theorem	biluk 899	Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96. (Contributed by NM, 10-Jan-2005.)
⊢ ((φ ↔ ψ) ↔ ((χ ↔ ψ) ↔ (φ ↔ χ)))
Theorem	pm5.7 900	Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 898. (Contributed by Roy F. Longton, 21-Jun-2005.)
⊢ (((φ ∨ χ) ↔ (ψ ∨ χ)) ↔ (χ ∨ (φ ↔ ψ)))