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.)
|- ((ph /\ (ps /\ ch)) <-> ((ph /\ ps) /\ (ph /\ ch)))
Theorem	anandir 802	Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
|- (((ph /\ ps) /\ ch) <-> ((ph /\ ch) /\ (ps /\ ch)))
Theorem	anandis 803	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- (((ph /\ ps) /\ (ph /\ ch)) -> ta)   =>   |- ((ph /\ (ps /\ ch)) -> ta)
Theorem	anandirs 804	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- (((ph /\ ch) /\ (ps /\ ch)) -> ta)   =>   |- (((ph /\ ps) /\ ch) -> ta)
Theorem	impbida 805	Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ch) -> ps)   =>   |- (ph -> (ps <-> ch))
Theorem	pm3.48 806	Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.)
|- (((ph -> ps) /\ (ch -> th)) -> ((ph \/ ch) -> (ps \/ th)))
Theorem	pm3.45 807	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ((ph -> ps) -> ((ph /\ ch) -> (ps /\ ch)))
Theorem	im2anan9 808	Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
|- (ph -> (ps -> ch))   &   |- (th -> (ta -> et))   =>   |- ((ph /\ th) -> ((ps /\ ta) -> (ch /\ et)))
Theorem	im2anan9r 809	Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
|- (ph -> (ps -> ch))   &   |- (th -> (ta -> et))   =>   |- ((th /\ ph) -> ((ps /\ ta) -> (ch /\ et)))
Theorem	anim12dan 810	Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ th) -> ta)   =>   |- ((ph /\ (ps /\ th)) -> (ch /\ ta))
Theorem	orim12d 811	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
|- (ph -> (ps -> ch))   &   |- (ph -> (th -> ta))   =>   |- (ph -> ((ps \/ th) -> (ch \/ ta)))
Theorem	orim1d 812	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
|- (ph -> (ps -> ch))   =>   |- (ph -> ((ps \/ th) -> (ch \/ th)))
Theorem	orim2d 813	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
|- (ph -> (ps -> ch))   =>   |- (ph -> ((th \/ ps) -> (th \/ ch)))
Theorem	orim2 814	Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)
|- ((ps -> ch) -> ((ph \/ ps) -> (ph \/ ch)))
Theorem	pm2.38 815	Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
|- ((ps -> ch) -> ((ps \/ ph) -> (ch \/ ph)))
Theorem	pm2.36 816	Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
|- ((ps -> ch) -> ((ph \/ ps) -> (ch \/ ph)))
Theorem	pm2.37 817	Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
|- ((ps -> ch) -> ((ps \/ ph) -> (ph \/ ch)))
Theorem	pm2.73 818	Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
|- ((ph -> ps) -> (((ph \/ ps) \/ ch) -> (ps \/ ch)))
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.)
|- ((ps -> ph) -> (((ph \/ ps) \/ ch) -> (ph \/ ch)))
Theorem	orimdi 820	Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.)
|- ((ph \/ (ps -> ch)) <-> ((ph \/ ps) -> (ph \/ ch)))
Theorem	pm2.76 821	Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
|- ((ph \/ (ps -> ch)) -> ((ph \/ ps) -> (ph \/ ch)))
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.)
|- ((ph \/ ps) -> ((ph \/ (ps -> ch)) -> (ph \/ ch)))
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.)
|- ((ph \/ ps) -> ((-. ps \/ ch) -> (ph \/ ch)))
Theorem	pm2.81 824	Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
|- ((ps -> (ch -> th)) -> ((ph \/ ps) -> ((ph \/ ch) -> (ph \/ th))))
Theorem	pm2.82 825	Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
|- (((ph \/ ps) \/ ch) -> (((ph \/ -. ch) \/ th) -> ((ph \/ ps) \/ th)))
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.)
|- (((ph \/ ps) -> (ph \/ ch)) -> (ph \/ (ps -> ch)))
Theorem	pm3.2ni 827	Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)
|- -. ph   &   |- -. ps   =>   |- -. (ph \/ ps)
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.)
|- (ph <-> ((ph \/ ps) /\ ph))
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.)
|- (((ph \/ -. ps) /\ ps) <-> (ph /\ ps))
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.)
|- ((ph /\ ps) -> (ph <-> ps))
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.)
|- ((-. ph /\ -. ps) -> (ph <-> ps))
Theorem	pm3.43 832	Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- (((ph -> ps) /\ (ph -> ch)) -> (ph -> (ps /\ ch)))
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.)
|- ((ph -> (ps /\ ch)) <-> ((ph -> ps) /\ (ph -> ch)))
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.)
|- ((ph \/ (ps /\ ch)) <-> ((ph \/ ps) /\ (ph \/ ch)))
Theorem	ordir 835	Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
|- (((ph /\ ps) \/ ch) <-> ((ph \/ ch) /\ (ps \/ ch)))
Theorem	pm4.76 836	Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
|- (((ph -> ps) /\ (ph -> ch)) <-> (ph -> (ps /\ ch)))
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.)
|- ((ph /\ (ps \/ ch)) <-> ((ph /\ ps) \/ (ph /\ ch)))
Theorem	andir 838	Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
|- (((ph \/ ps) /\ ch) <-> ((ph /\ ch) \/ (ps /\ ch)))
Theorem	orddi 839	Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
|- (((ph /\ ps) \/ (ch /\ th)) <-> (((ph \/ ch) /\ (ph \/ th)) /\ ((ps \/ ch) /\ (ps \/ th))))
Theorem	anddi 840	Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
|- (((ph \/ ps) /\ (ch \/ th)) <-> (((ph /\ ch) \/ (ph /\ th)) \/ ((ps /\ ch) \/ (ps /\ th))))
Theorem	pm4.39 841	Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- (((ph <-> ch) /\ (ps <-> th)) -> ((ph \/ ps) <-> (ch \/ th)))
Theorem	pm4.38 842	Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- (((ph <-> ch) /\ (ps <-> th)) -> ((ph /\ ps) <-> (ch /\ th)))
Theorem	bi2anan9 843	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
|- (ph -> (ps <-> ch))   &   |- (th -> (ta <-> et))   =>   |- ((ph /\ th) -> ((ps /\ ta) <-> (ch /\ et)))
Theorem	bi2anan9r 844	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.)
|- (ph -> (ps <-> ch))   &   |- (th -> (ta <-> et))   =>   |- ((th /\ ph) -> ((ps /\ ta) <-> (ch /\ et)))
Theorem	bi2bian9 845	Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.)
|- (ph -> (ps <-> ch))   &   |- (th -> (ta <-> et))   =>   |- ((ph /\ th) -> ((ps <-> ta) <-> (ch <-> et)))
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.)
|- ((ph -> ps) <-> (ps <-> (ph \/ ps)))
Theorem	imimorb 847	Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
|- (((ps -> ch) -> (ph -> ch)) <-> (ph -> (ps \/ ch)))
Theorem	pm5.33 848	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ((ph /\ (ps -> ch)) <-> (ph /\ ((ph /\ ps) -> ch)))
Theorem	pm5.36 849	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ((ph /\ (ph <-> ps)) <-> (ps /\ (ph <-> ps)))
Theorem	bianabs 850	Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)
|- (ph -> (ps <-> (ph /\ ch)))   =>   |- (ph -> (ps <-> ch))
Theorem	oibabs 851	Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
|- (((ph \/ ps) -> (ph <-> ps)) <-> (ph <-> ps))
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.)
|- -. (ph /\ -. ph)
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.)
|- (-. ph \/ ((ph -> ps) -> ps))
Theorem	pm5.11 854	Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
|- ((ph -> ps) \/ (-. ph -> ps))
Theorem	pm5.12 855	Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
|- ((ph -> ps) \/ (ph -> -. ps))
Theorem	pm5.14 856	Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
|- ((ph -> ps) \/ (ps -> ch))
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.)
|- ((ph -> ps) \/ (ps -> ph))
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.)
|- (((ph \/ ps) /\ -. (ph /\ ps)) <-> (ph <-> -. ps))
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.)
|- ((ph <-> ps) \/ (ph <-> -. ps))
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.)
|- -. ((ph <-> ps) /\ (ph <-> -. ps))
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.)
|- (-. (ph <-> ps) <-> ((ph /\ -. ps) \/ (ps /\ -. ph)))
Theorem	nbi2 862	Two ways to express "exclusive or." (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
|- (-. (ph <-> ps) <-> ((ph \/ ps) /\ -. (ph /\ ps)))
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.)
|- ((ph <-> ps) <-> ((ph /\ ps) \/ (-. ph /\ -. ps)))
Theorem	pm5.24 864	Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)
|- (-. ((ph /\ ps) \/ (-. ph /\ -. ps)) <-> ((ph /\ -. ps) \/ (ps /\ -. ph)))
Theorem	xordi 865	Conjunction distributes over exclusive-or, using -. (ph <-> ps) 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.)
|- ((ph /\ -. (ps <-> ch)) <-> -. ((ph /\ ps) <-> (ph /\ ch)))
Theorem	biort 866	A wff disjoined with truth is true. (Contributed by NM, 23-May-1999.)
|- (ph -> (ph <-> (ph \/ ps)))
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.)
|- (((ph \/ ps) <-> ph) \/ ((ph \/ ps) <-> ps))
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.)
|- ((ph /\ ps) -> th)   &   |- ((ph /\ ch) -> th)   &   |- (th -> (ps <-> ch))   =>   |- (ph -> (ps <-> ch))
Theorem	pm5.35 869	Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- (((ph -> ps) /\ (ph -> ch)) -> (ph -> (ps <-> ch)))
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.)
|- (((ph /\ ps) <-> ph) \/ ((ph /\ ps) <-> ps))
Theorem	baib 871	Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
|- (ph <-> (ps /\ ch))   =>   |- (ps -> (ph <-> ch))
Theorem	baibr 872	Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
|- (ph <-> (ps /\ ch))   =>   |- (ps -> (ch <-> ph))
Theorem	rbaib 873	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- (ph <-> (ps /\ ch))   =>   |- (ch -> (ph <-> ps))
Theorem	rbaibr 874	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- (ph <-> (ps /\ ch))   =>   |- (ch -> (ps <-> ph))
Theorem	baibd 875	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- (ph -> (ps <-> (ch /\ th)))   =>   |- ((ph /\ ch) -> (ps <-> th))
Theorem	rbaibd 876	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- (ph -> (ps <-> (ch /\ th)))   =>   |- ((ph /\ th) -> (ps <-> ch))
Theorem	pm5.44 877	Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ((ph -> ps) -> ((ph -> ch) <-> (ph -> (ps /\ ch))))
Theorem	pm5.6 878	Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.)
|- (((ph /\ -. ps) -> ch) <-> (ph -> (ps \/ ch)))
Theorem	orcanai 879	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
|- (ph -> (ps \/ ch))   =>   |- ((ph /\ -. ps) -> ch)
Theorem	intnan 880	Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
|- -. ph   =>   |- -. (ps /\ ph)
Theorem	intnanr 881	Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
|- -. ph   =>   |- -. (ph /\ ps)
Theorem	intnand 882	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- (ph -> -. ps)   =>   |- (ph -> -. (ch /\ ps))
Theorem	intnanrd 883	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- (ph -> -. ps)   =>   |- (ph -> -. (ps /\ ch))
Theorem	mpbiran 884	Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)
|- ps   &   |- (ph <-> (ps /\ ch))   =>   |- (ph <-> ch)
Theorem	mpbiran2 885	Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)
|- ch   &   |- (ph <-> (ps /\ ch))   =>   |- (ph <-> ps)
Theorem	mpbir2an 886	Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
|- ps   &   |- ch   &   |- (ph <-> (ps /\ ch))   =>   |- ph
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.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> ((ps /\ ch) <-> th))   =>   |- (ph -> th)
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.)
|- (ph -> ch)   &   |- (ph -> th)   &   |- (ph -> (ps <-> (ch /\ th)))   =>   |- (ph -> ps)
Theorem	pm5.62 889	Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)
|- (((ph /\ ps) \/ -. ps) <-> (ph \/ -. ps))
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.)
|- ((ph \/ ps) <-> (ph \/ (-. ph /\ ps)))
Theorem	bianfi 891	A wff conjoined with falsehood is false. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|- -. ph   =>   |- (ph <-> (ps /\ ph))
Theorem	bianfd 892	A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
|- (ph -> -. ps)   =>   |- (ph -> (ps <-> (ps /\ ch)))
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.)
|- (ph <-> ((ph \/ ps) /\ (ph \/ -. ps)))
Theorem	pm4.82 894	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
|- (((ph -> ps) /\ (ph -> -. ps)) <-> -. ph)
Theorem	pm4.83 895	Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
|- (((ph -> ps) /\ (-. ph -> ps)) <-> ps)
Theorem	pclem6 896	Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.)
|- ((ph <-> (ps /\ -. ph)) -> -. ps)
Theorem	biantr 897	A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)
|- (((ph <-> ps) /\ (ch <-> ps)) -> (ph <-> ch))
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.)
|- ((ph \/ (ps <-> ch)) <-> ((ph \/ ps) <-> (ph \/ ch)))
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.)
|- ((ph <-> ps) <-> ((ch <-> ps) <-> (ph <-> ch)))
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.)
|- (((ph \/ ch) <-> (ps \/ ch)) <-> (ch \/ (ph <-> ps)))