P. 10 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 901-1000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oranabs 901	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 902	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 903	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	norbi 904	If neither of two propositions is true, then these propositions are equivalent. (Contributed by BJ, 26-Apr-2019.)
|- ( -. ( ph \/ ps ) -> ( ph <-> ps ) )
Theorem	nbior 905	If two propositions are not equivalent, then at least one is true. (Contributed by BJ, 19-Apr-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
|- ( -. ( ph <-> ps ) -> ( ph \/ ps ) )
Theorem	pm3.43 906	Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) -> ( ph -> ( ps /\ ch ) ) )
Theorem	jcab 907	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 908	Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Jan-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 909	Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
|- ( ( ( ph /\ ps ) \/ ch ) <-> ( ( ph \/ ch ) /\ ( ps \/ ch ) ) )
Theorem	pm4.76 910	Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
Theorem	andi 911	Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
|- ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
Theorem	andir 912	Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
|- ( ( ( ph \/ ps ) /\ ch ) <-> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) )
Theorem	orddi 913	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 914	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 915	Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ( ph \/ ps ) <-> ( ch \/ th ) ) )
Theorem	pm4.38 916	Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ( ph /\ ps ) <-> ( ch /\ th ) ) )
Theorem	bi2anan9 917	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 918	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 919	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 920	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 921	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 922	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph /\ ( ps -> ch ) ) <-> ( ph /\ ( ( ph /\ ps ) -> ch ) ) )
Theorem	pm5.36 923	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph /\ ( ph <-> ps ) ) <-> ( ps /\ ( ph <-> ps ) ) )
Theorem	bianabs 924	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 925	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 926	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 927	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 928	Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) \/ ( -. ph -> ps ) )
Theorem	pm5.12 929	Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) \/ ( ph -> -. ps ) )
Theorem	pm5.14 930	Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) \/ ( ps -> ch ) )
Theorem	pm5.13 931	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 932	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 933	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 934	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 935	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 936	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	xordi 937	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. This is not necessarily true in intuitionistic logic, though anxordi 1479 does hold in it. (Contributed by NM, 3-Oct-2008.)
|- ( ( ph /\ -. ( ps <-> ch ) ) <-> -. ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )
Theorem	biort 938	A wff disjoined with truth is true. (Contributed by NM, 23-May-1999.)
|- ( ph -> ( ph <-> ( ph \/ ps ) ) )
Theorem	pm5.55 939	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 ) )
Theorem	ornld 940	Selecting one statement from a disjunction if one of the disjuncted statements is false. (Contributed by AV, 6-Sep-2018.) (Proof shortened by AV, 13-Oct-2018.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
|- ( ph -> ( ( ( ph -> ( th \/ ta ) ) /\ -. th ) -> ta ) )
Theorem	pm5.21nd 941	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 942	Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) -> ( ph -> ( ps <-> ch ) ) )
Theorem	pm5.54 943	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 944	Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ph <-> ch ) )
Theorem	baibr 945	Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ch <-> ph ) )
Theorem	rbaibr 946	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ps <-> ph ) )
Theorem	rbaib 947	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ph <-> ps ) )
Theorem	baibd 948	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ch ) -> ( ps <-> th ) )
Theorem	rbaibd 949	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ th ) -> ( ps <-> ch ) )
Theorem	pm5.44 950	Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ph -> ch ) <-> ( ph -> ( ps /\ ch ) ) ) )
Theorem	pm5.6 951	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 952	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
|- ( ph -> ( ps \/ ch ) )   =>    |- ( ( ph /\ -. ps ) -> ch )
Theorem	mpbiran 953	Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)
|- ps   &    |- ( ph <-> ( ps /\ ch ) )   =>    |- ( ph <-> ch )
Theorem	mpbiran2 954	Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)
|- ch   &    |- ( ph <-> ( ps /\ ch ) )   =>    |- ( ph <-> ps )
Theorem	mpbir2an 955	Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
|- ps   &    |- ch   &    |- ( ph <-> ( ps /\ ch ) )   =>    |- ph
Theorem	mpbi2and 956	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 957	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 )
1.2.7  Miscellaneous theorems of propositional calculus This subsection gathers miscellaneous theorems of propositional calculus, including proofs by cases and other theorems with negated wffs.
Theorem	pm5.62 958	Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)
|- ( ( ( ph /\ ps ) \/ -. ps ) <-> ( ph \/ -. ps ) )
Theorem	pm5.63 959	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	intnan 960	Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
|- -. ph   =>    |- -. ( ps /\ ph )
Theorem	intnanr 961	Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
|- -. ph   =>    |- -. ( ph /\ ps )
Theorem	intnand 962	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ch /\ ps ) )
Theorem	intnanrd 963	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ps /\ ch ) )
Theorem	niabn 964	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>    |- ( -. ps -> ( ( ch /\ ps ) <-> -. ph ) )
Theorem	ninba 965	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>    |- ( -. ps -> ( -. ph <-> ( ch /\ ps ) ) )
Theorem	bianfi 966	A wff conjoined with falsehood is false. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|- -. ph   =>    |- ( ph <-> ( ps /\ ph ) )
Theorem	bianfd 967	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 968	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 969	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> -. ps ) ) <-> -. ph )
Theorem	pm4.83 970	Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( -. ph -> ps ) ) <-> ps )
Theorem	pclem6 971	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 972	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 973	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 974	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 975	Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 973. (Contributed by Roy F. Longton, 21-Jun-2005.)
|- ( ( ( ph \/ ch ) <-> ( ps \/ ch ) ) <-> ( ch \/ ( ph <-> ps ) ) )
Theorem	bigolden 976	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
|- ( ( ( ph /\ ps ) <-> ph ) <-> ( ps <-> ( ph \/ ps ) ) )
Theorem	pm5.71 977	Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.)
|- ( ( ps -> -. ch ) -> ( ( ( ph \/ ps ) /\ ch ) <-> ( ph /\ ch ) ) )
Theorem	pm5.75 978	Theorem *5.75 of [WhiteheadRussell] p. 126. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2012.) (Proof shortened by Kyle Wyonch, 12-Feb-2021.)
|- ( ( ( ch -> -. ps ) /\ ( ph <-> ( ps \/ ch ) ) ) -> ( ( ph /\ -. ps ) <-> ch ) )
Theorem	pm5.75OLD 979	Obsolete proof of pm5.75 978 as of 12-Feb-2021. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2012.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( ch -> -. ps ) /\ ( ph <-> ( ps \/ ch ) ) ) -> ( ( ph /\ -. ps ) <-> ch ) )
Theorem	bimsc1 980	Removal of conjunct from one side of an equivalence. (Contributed by NM, 21-Jun-1993.)
|- ( ( ( ph -> ps ) /\ ( ch <-> ( ps /\ ph ) ) ) -> ( ch <-> ph ) )
Theorem	ecase2d 981	Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Dec-2012.)
|- ( ph -> ps )   &    |- ( ph -> -. ( ps /\ ch ) )   &    |- ( ph -> -. ( ps /\ th ) )   &    |- ( ph -> ( ta \/ ( ch \/ th ) ) )   =>    |- ( ph -> ta )
Theorem	ecase3 982	Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|- ( ph -> ch )   &    |- ( ps -> ch )   &    |- ( -. ( ph \/ ps ) -> ch )   =>    |- ch
Theorem	ecase 983	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
|- ( -. ph -> ch )   &    |- ( -. ps -> ch )   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ch
Theorem	ecase3d 984	Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( ph -> ( ps -> th ) )   &    |- ( ph -> ( ch -> th ) )   &    |- ( ph -> ( -. ( ps \/ ch ) -> th ) )   =>    |- ( ph -> th )
Theorem	ecased 985	Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.)
|- ( ph -> ( -. ps -> th ) )   &    |- ( ph -> ( -. ch -> th ) )   &    |- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> th )
Theorem	ecase3ad 986	Deduction for elimination by cases. (Contributed by NM, 24-May-2013.)
|- ( ph -> ( ps -> th ) )   &    |- ( ph -> ( ch -> th ) )   &    |- ( ph -> ( ( -. ps /\ -. ch ) -> th ) )   =>    |- ( ph -> th )
Theorem	ccase 987	Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
|- ( ( ph /\ ps ) -> ta )   &    |- ( ( ch /\ ps ) -> ta )   &    |- ( ( ph /\ th ) -> ta )   &    |- ( ( ch /\ th ) -> ta )   =>    |- ( ( ( ph \/ ch ) /\ ( ps \/ th ) ) -> ta )
Theorem	ccased 988	Deduction for combining cases. (Contributed by NM, 9-May-2004.)
|- ( ph -> ( ( ps /\ ch ) -> et ) )   &    |- ( ph -> ( ( th /\ ch ) -> et ) )   &    |- ( ph -> ( ( ps /\ ta ) -> et ) )   &    |- ( ph -> ( ( th /\ ta ) -> et ) )   =>    |- ( ph -> ( ( ( ps \/ th ) /\ ( ch \/ ta ) ) -> et ) )
Theorem	ccase2 989	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|- ( ( ph /\ ps ) -> ta )   &    |- ( ch -> ta )   &    |- ( th -> ta )   =>    |- ( ( ( ph \/ ch ) /\ ( ps \/ th ) ) -> ta )
Theorem	4cases 990	Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ -. ps ) -> ch )   &    |- ( ( -. ph /\ ps ) -> ch )   &    |- ( ( -. ph /\ -. ps ) -> ch )   =>    |- ch
Theorem	4casesdan 991	Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   &    |- ( ( ph /\ ( ps /\ -. ch ) ) -> th )   &    |- ( ( ph /\ ( -. ps /\ ch ) ) -> th )   &    |- ( ( ph /\ ( -. ps /\ -. ch ) ) -> th )   =>    |- ( ph -> th )
Theorem	cases 992	Case disjunction according to the value of ph. (Contributed by NM, 25-Apr-2019.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( -. ph -> ( ps <-> th ) )   =>    |- ( ps <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )
Theorem	cases2 993	Case disjunction according to the value of ph. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 2-Jan-2020.)
|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
Theorem	dfbi3 994	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.) (Proof shortened by NM, 29-Oct-2021.)
|- ( ( ph <-> ps ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) )
Theorem	dfbi3OLD 995	Obsolete proof of dfbi3 994 as of 29-Oct-2021. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) )
Theorem	pm5.24 996	Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) <-> ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) )
Theorem	4exmid 997	The disjunction of the four possible combinations of two wffs and their negations is always true. A four-way excluded middle (see exmid 431). (Contributed by David Abernethy, 28-Jan-2014.) (Proof shortened by NM, 29-Oct-2021.)
|- ( ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) \/ ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) )
Theorem	4exmidOLD 998	Obsolete proof of 4exmid 997 as of 29-Oct-2021. (Contributed by David Abernethy, 28-Jan-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) \/ ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) )
Theorem	consensus 999	The consensus theorem. This theorem and its dual (with \/ and /\ interchanged) are commonly used in computer logic design to eliminate redundant terms from Boolean expressions. Specifically, we prove that the term ( ps /\ ch ) on the left-hand side is redundant. (Contributed by NM, 16-May-2003.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)
|- ( ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) \/ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
Theorem	dedlem0a 1000	Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|- ( ph -> ( ps <-> ( ( ch -> ph ) -> ( ps /\ ph ) ) ) )