P. 8 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 701-800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imnan 701	Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.)
|- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )
Theorem	imnani 702	Express implication in terms of conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.)
|- -. ( ph /\ ps )   =>    |- ( ph -> -. ps )
Theorem	nan 703	Theorem to move a conjunct in and out of a negation. (Contributed by NM, 9-Nov-2003.)
|- ( ( ph -> -. ( ps /\ ch ) ) <-> ( ( ph /\ ps ) -> -. ch ) )
Theorem	mpnanrd 704	Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020.)
|- ( ph -> ps )   &    |- ( ph -> -. ( ps /\ ch ) )   =>    |- ( ph -> -. ch )
Theorem	pm3.24 705	Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 2-Feb-2015.)
|- -. ( ph /\ -. ph )
Theorem	pm4.15 706	Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
|- ( ( ( ph /\ ps ) -> -. ch ) <-> ( ( ps /\ ch ) -> -. ph ) )
Theorem	pm5.21 707	Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124. (Contributed by NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ( -. ph /\ -. ps ) -> ( ph <-> ps ) )
Theorem	pm5.21im 708	Two propositions are equivalent if they are both false. Closed form of 2false 713. Equivalent to a biimpr 130-like version of the xor-connective. (Contributed by Wolf Lammen, 13-May-2013.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( -. ph -> ( -. ps -> ( ph <-> ps ) ) )
Theorem	nbn2 709	The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) )
Theorem	bibif 710	Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.) (Proof shortened by Wolf Lammen, 28-Jan-2013.)
|- ( -. ps -> ( ( ph <-> ps ) <-> -. ph ) )
Theorem	nbn 711	The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|- -. ph   =>    |- ( -. ps <-> ( ps <-> ph ) )
Theorem	nbn3 712	Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.)
|- ph   =>    |- ( -. ps <-> ( ps <-> -. ph ) )
Theorem	2false 713	Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- -. ph   &    |- -. ps   =>    |- ( ph <-> ps )
Theorem	2falsed 714	Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.)
|- ( ph -> -. ps )   &    |- ( ph -> -. ch )   =>    |- ( ph -> ( ps <-> ch ) )
Theorem	pm5.21ni 715	Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.)
|- ( ph -> ps )   &    |- ( ch -> ps )   =>    |- ( -. ps -> ( ph <-> ch ) )
Theorem	pm5.21nii 716	Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph -> ps )   &    |- ( ch -> ps )   &    |- ( ps -> ( ph <-> ch ) )   =>    |- ( ph <-> ch )
Theorem	pm5.21ndd 717	Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph -> ( ch -> ps ) )   &    |- ( ph -> ( th -> ps ) )   &    |- ( ph -> ( ps -> ( ch <-> th ) ) )   =>    |- ( ph -> ( ch <-> th ) )
Theorem	pm5.19 718	Theorem *5.19 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- -. ( ph <-> -. ph )
Theorem	pm4.8 719	Theorem *4.8 of [WhiteheadRussell] p. 122. This one holds for all propositions, but compare with pm4.81dc 920 which requires a decidability condition. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> -. ph ) <-> -. ph )
1.2.6  Logical disjunction
Syntax	wo 720	Extend wff definition to include disjunction ('or').
wff ( ph \/ ps )
Axiom	ax-io 721	Definition of 'or'. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias jaob 722 instead. (New usage is discouraged.)
|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
Theorem	jaob 722	Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121. Alias of ax-io 721. (Contributed by NM, 30-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
Theorem	olc 723	Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
|- ( ph -> ( ps \/ ph ) )
Theorem	orc 724	Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
|- ( ph -> ( ph \/ ps ) )
Theorem	pm2.67-2 725	Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
|- ( ( ( ph \/ ch ) -> ps ) -> ( ph -> ps ) )
Theorem	oibabs 726	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.44 727	Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|- ( ( ( ps -> ph ) /\ ( ch -> ph ) ) -> ( ( ps \/ ch ) -> ph ) )
Theorem	jaoi 728	Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.)
|- ( ph -> ps )   &    |- ( ch -> ps )   =>    |- ( ( ph \/ ch ) -> ps )
Theorem	jaod 729	Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( th -> ch ) )   =>    |- ( ph -> ( ( ps \/ th ) -> ch ) )
Theorem	mpjaod 730	Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( th -> ch ) )   &    |- ( ph -> ( ps \/ th ) )   =>    |- ( ph -> ch )
Theorem	jaao 731	Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ( ta -> ch ) )   =>    |- ( ( ph /\ th ) -> ( ( ps \/ ta ) -> ch ) )
Theorem	jaoa 732	Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ( ta -> ch ) )   =>    |- ( ( ph \/ th ) -> ( ( ps /\ ta ) -> ch ) )
Theorem	imorr 733	Implication in terms of disjunction. One direction of theorem *4.6 of [WhiteheadRussell] p. 120. The converse holds for decidable propositions, as seen at imordc 909. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- ( ( -. ph \/ ps ) -> ( ph -> ps ) )
Theorem	pm2.53 734	Theorem *2.53 of [WhiteheadRussell] p. 107. This holds intuitionistically, although its converse does not (see pm2.54dc 903). (Contributed by NM, 3-Jan-2005.) (Revised by NM, 31-Jan-2015.)
|- ( ( ph \/ ps ) -> ( -. ph -> ps ) )
Theorem	ori 735	Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph \/ ps )   =>    |- ( -. ph -> ps )
Theorem	ord 736	Deduce implication from disjunction. (Contributed by NM, 18-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph -> ( ps \/ ch ) )   =>    |- ( ph -> ( -. ps -> ch ) )
Theorem	orel1 737	Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 21-Jul-2012.)
|- ( -. ph -> ( ( ph \/ ps ) -> ps ) )
Theorem	orel2 738	Elimination of disjunction by denial of a disjunct. Theorem *2.56 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 5-Apr-2013.)
|- ( -. ph -> ( ( ps \/ ph ) -> ps ) )
Theorem	pm1.4 739	Axiom *1.4 of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 15-Nov-2012.)
|- ( ( ph \/ ps ) -> ( ps \/ ph ) )
Theorem	orcom 740	Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.)
|- ( ( ph \/ ps ) <-> ( ps \/ ph ) )
Theorem	orcomd 741	Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)
|- ( ph -> ( ps \/ ch ) )   =>    |- ( ph -> ( ch \/ ps ) )
Theorem	orcoms 742	Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012.)
|- ( ( ph \/ ps ) -> ch )   =>    |- ( ( ps \/ ph ) -> ch )
Theorem	orci 743	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>    |- ( ph \/ ps )
Theorem	olci 744	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>    |- ( ps \/ ph )
Theorem	orcd 745	Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
|- ( ph -> ps )   =>    |- ( ph -> ( ps \/ ch ) )
Theorem	olcd 746	Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|- ( ph -> ps )   =>    |- ( ph -> ( ch \/ ps ) )
Theorem	orcs 747	Deduction eliminating disjunct. Notational convention: We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 14) -type inference in a proof. (Contributed by NM, 21-Jun-1994.)
|- ( ( ph \/ ps ) -> ch )   =>    |- ( ph -> ch )
Theorem	olcs 748	Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|- ( ( ph \/ ps ) -> ch )   =>    |- ( ps -> ch )
Theorem	pm2.07 749	Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
|- ( ph -> ( ph \/ ph ) )
Theorem	pm2.45 750	Theorem *2.45 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> -. ph )
Theorem	pm2.46 751	Theorem *2.46 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> -. ps )
Theorem	pm2.47 752	Theorem *2.47 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> ( -. ph \/ ps ) )
Theorem	pm2.48 753	Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> ( ph \/ -. ps ) )
Theorem	pm2.49 754	Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> ( -. ph \/ -. ps ) )
Theorem	pm2.67 755	Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
|- ( ( ( ph \/ ps ) -> ps ) -> ( ph -> ps ) )
Theorem	biorf 756	A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
|- ( -. ph -> ( ps <-> ( ph \/ ps ) ) )
Theorem	biortn 757	A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.)
|- ( ph -> ( ps <-> ( -. ph \/ ps ) ) )
Theorem	biorfi 758	A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.)
|- -. ph   =>    |- ( ps <-> ( ps \/ ph ) )
Theorem	pm2.621 759	Theorem *2.621 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 13-Dec-2013.)
|- ( ( ph -> ps ) -> ( ( ph \/ ps ) -> ps ) )
Theorem	pm2.62 760	Theorem *2.62 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.)
|- ( ( ph \/ ps ) -> ( ( ph -> ps ) -> ps ) )
Theorem	imorri 761	Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( -. ph \/ ps )   =>    |- ( ph -> ps )
Theorem	pm4.52im 762	One direction of theorem *4.52 of [WhiteheadRussell] p. 120. The converse also holds in classical logic. (Contributed by Jim Kingdon, 27-Jul-2018.)
|- ( ( ph /\ -. ps ) -> -. ( -. ph \/ ps ) )
Theorem	pm4.53r 763	One direction of theorem *4.53 of [WhiteheadRussell] p. 120. The converse also holds in classical logic. (Contributed by Jim Kingdon, 27-Jul-2018.)
|- ( ( -. ph \/ ps ) -> -. ( ph /\ -. ps ) )
Theorem	ioran 764	Negated disjunction in terms of conjunction. This version of DeMorgan's law is a biconditional for all propositions (not just decidable ones), unlike oranim 793, anordc 969, or ianordc 911. Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )
Theorem	pm3.14 765	Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 911. The converse holds for decidable propositions, as seen at pm3.13dc 972. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ( -. ph \/ -. ps ) -> -. ( ph /\ ps ) )
Theorem	pm3.1 766	Theorem *3.1 of [WhiteheadRussell] p. 111. The converse holds for decidable propositions, as seen at anordc 969. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ( ph /\ ps ) -> -. ( -. ph \/ -. ps ) )
Theorem	jao 767	Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 4-Apr-2013.)
|- ( ( ph -> ps ) -> ( ( ch -> ps ) -> ( ( ph \/ ch ) -> ps ) ) )
Theorem	pm1.2 768	Axiom *1.2 (Taut) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 10-Mar-2013.)
|- ( ( ph \/ ph ) -> ph )
Theorem	oridm 769	Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.)
|- ( ( ph \/ ph ) <-> ph )
Theorem	pm4.25 770	Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph \/ ph ) )
Theorem	orim12i 771	Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
|- ( ph -> ps )   &    |- ( ch -> th )   =>    |- ( ( ph \/ ch ) -> ( ps \/ th ) )
Theorem	orim1i 772	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
|- ( ph -> ps )   =>    |- ( ( ph \/ ch ) -> ( ps \/ ch ) )
Theorem	orim2i 773	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
|- ( ph -> ps )   =>    |- ( ( ch \/ ph ) -> ( ch \/ ps ) )
Theorem	orbi2i 774	Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)
|- ( ph <-> ps )   =>    |- ( ( ch \/ ph ) <-> ( ch \/ ps ) )
Theorem	orbi1i 775	Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   =>    |- ( ( ph \/ ch ) <-> ( ps \/ ch ) )
Theorem	orbi12i 776	Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph \/ ch ) <-> ( ps \/ th ) )
Theorem	pm1.5 777	Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ps \/ ch ) ) -> ( ps \/ ( ph \/ ch ) ) )
Theorem	or12 778	Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
|- ( ( ph \/ ( ps \/ ch ) ) <-> ( ps \/ ( ph \/ ch ) ) )
Theorem	orass 779	Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )
Theorem	pm2.31 780	Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ps \/ ch ) ) -> ( ( ph \/ ps ) \/ ch ) )
Theorem	pm2.32 781	Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph \/ ps ) \/ ch ) -> ( ph \/ ( ps \/ ch ) ) )
Theorem	or32 782	A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( ( ph \/ ps ) \/ ch ) <-> ( ( ph \/ ch ) \/ ps ) )
Theorem	or4 783	Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
|- ( ( ( ph \/ ps ) \/ ( ch \/ th ) ) <-> ( ( ph \/ ch ) \/ ( ps \/ th ) ) )
Theorem	or42 784	Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
|- ( ( ( ph \/ ps ) \/ ( ch \/ th ) ) <-> ( ( ph \/ ch ) \/ ( th \/ ps ) ) )
Theorem	orordi 785	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
|- ( ( ph \/ ( ps \/ ch ) ) <-> ( ( ph \/ ps ) \/ ( ph \/ ch ) ) )
Theorem	orordir 786	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
|- ( ( ( ph \/ ps ) \/ ch ) <-> ( ( ph \/ ch ) \/ ( ps \/ ch ) ) )
Theorem	pm2.3 787	Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ps \/ ch ) ) -> ( ph \/ ( ch \/ ps ) ) )
Theorem	pm2.41 788	Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( ( ps \/ ( ph \/ ps ) ) -> ( ph \/ ps ) )
Theorem	pm2.42 789	Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( ( -. ph \/ ( ph -> ps ) ) -> ( ph -> ps ) )
Theorem	pm2.4 790	Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ph \/ ps ) ) -> ( ph \/ ps ) )
Theorem	pm4.44 791	Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph \/ ( ph /\ ps ) ) )
Theorem	pm4.56 792	Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- ( ( -. ph /\ -. ps ) <-> -. ( ph \/ ps ) )
Theorem	oranim 793	Disjunction in terms of conjunction (DeMorgan's law). One direction of Theorem *4.57 of [WhiteheadRussell] p. 120. The converse does not hold intuitionistically but does hold in classical logic. (Contributed by Jim Kingdon, 25-Jul-2018.)
|- ( ( ph \/ ps ) -> -. ( -. ph /\ -. ps ) )
Theorem	pm4.78i 794	Implication distributes over disjunction. One direction of Theorem *4.78 of [WhiteheadRussell] p. 121. The converse holds in classical logic. (Contributed by Jim Kingdon, 15-Jan-2018.)
|- ( ( ( ph -> ps ) \/ ( ph -> ch ) ) -> ( ph -> ( ps \/ ch ) ) )
Theorem	mtord 795	A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph -> -. ch )   &    |- ( ph -> -. th )   &    |- ( ph -> ( ps -> ( ch \/ th ) ) )   =>    |- ( ph -> -. ps )
Theorem	pm4.45 796	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph /\ ( ph \/ ps ) ) )
Theorem	pm3.48 797	Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) (Revised by NM, 1-Dec-2012.)
|- ( ( ( ph -> ps ) /\ ( ch -> th ) ) -> ( ( ph \/ ch ) -> ( ps \/ th ) ) )
Theorem	orim12d 798	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 799	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( ps \/ th ) -> ( ch \/ th ) ) )
Theorem	orim2d 800	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )