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	orc 701	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 702	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 703	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 704	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 705	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 706	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 707	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 708	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 709	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 710	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 882. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- ( ( -. ph \/ ps ) -> ( ph -> ps ) )
Theorem	pm2.53 711	Theorem *2.53 of [WhiteheadRussell] p. 107. This holds intuitionistically, although its converse does not (see pm2.54dc 876). (Contributed by NM, 3-Jan-2005.) (Revised by NM, 31-Jan-2015.)
|- ( ( ph \/ ps ) -> ( -. ph -> ps ) )
Theorem	ori 712	Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph \/ ps )   =>    |- ( -. ph -> ps )
Theorem	ord 713	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 714	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 715	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 716	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 717	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 718	Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)
|- ( ph -> ( ps \/ ch ) )   =>    |- ( ph -> ( ch \/ ps ) )
Theorem	orcoms 719	Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012.)
|- ( ( ph \/ ps ) -> ch )   =>    |- ( ( ps \/ ph ) -> ch )
Theorem	orci 720	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>    |- ( ph \/ ps )
Theorem	olci 721	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>    |- ( ps \/ ph )
Theorem	orcd 722	Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
|- ( ph -> ps )   =>    |- ( ph -> ( ps \/ ch ) )
Theorem	olcd 723	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 724	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 725	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 726	Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
|- ( ph -> ( ph \/ ph ) )
Theorem	pm2.45 727	Theorem *2.45 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> -. ph )
Theorem	pm2.46 728	Theorem *2.46 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> -. ps )
Theorem	pm2.47 729	Theorem *2.47 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> ( -. ph \/ ps ) )
Theorem	pm2.48 730	Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> ( ph \/ -. ps ) )
Theorem	pm2.49 731	Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> ( -. ph \/ -. ps ) )
Theorem	pm2.67 732	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 733	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 734	A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.)
|- ( ph -> ( ps <-> ( -. ph \/ ps ) ) )
Theorem	biorfi 735	A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.)
|- -. ph   =>    |- ( ps <-> ( ps \/ ph ) )
Theorem	pm2.621 736	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 737	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 738	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 739	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 740	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 741	Negated disjunction in terms of conjunction. This version of DeMorgan's law is a biconditional for all propositions (not just decidable ones), unlike oranim 770, anordc 940, or ianordc 884. 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 742	Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 884. The converse holds for decidable propositions, as seen at pm3.13dc 943. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ( -. ph \/ -. ps ) -> -. ( ph /\ ps ) )
Theorem	pm3.1 743	Theorem *3.1 of [WhiteheadRussell] p. 111. The converse holds for decidable propositions, as seen at anordc 940. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ( ph /\ ps ) -> -. ( -. ph \/ -. ps ) )
Theorem	jao 744	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 745	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 746	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 747	Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph \/ ph ) )
Theorem	orim12i 748	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 749	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
|- ( ph -> ps )   =>    |- ( ( ph \/ ch ) -> ( ps \/ ch ) )
Theorem	orim2i 750	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
|- ( ph -> ps )   =>    |- ( ( ch \/ ph ) -> ( ch \/ ps ) )
Theorem	orbi2i 751	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 752	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 753	Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph \/ ch ) <-> ( ps \/ th ) )
Theorem	pm1.5 754	Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ps \/ ch ) ) -> ( ps \/ ( ph \/ ch ) ) )
Theorem	or12 755	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 756	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 757	Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ps \/ ch ) ) -> ( ( ph \/ ps ) \/ ch ) )
Theorem	pm2.32 758	Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph \/ ps ) \/ ch ) -> ( ph \/ ( ps \/ ch ) ) )
Theorem	or32 759	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 760	Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
|- ( ( ( ph \/ ps ) \/ ( ch \/ th ) ) <-> ( ( ph \/ ch ) \/ ( ps \/ th ) ) )
Theorem	or42 761	Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
|- ( ( ( ph \/ ps ) \/ ( ch \/ th ) ) <-> ( ( ph \/ ch ) \/ ( th \/ ps ) ) )
Theorem	orordi 762	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
|- ( ( ph \/ ( ps \/ ch ) ) <-> ( ( ph \/ ps ) \/ ( ph \/ ch ) ) )
Theorem	orordir 763	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
|- ( ( ( ph \/ ps ) \/ ch ) <-> ( ( ph \/ ch ) \/ ( ps \/ ch ) ) )
Theorem	pm2.3 764	Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ps \/ ch ) ) -> ( ph \/ ( ch \/ ps ) ) )
Theorem	pm2.41 765	Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( ( ps \/ ( ph \/ ps ) ) -> ( ph \/ ps ) )
Theorem	pm2.42 766	Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( ( -. ph \/ ( ph -> ps ) ) -> ( ph -> ps ) )
Theorem	pm2.4 767	Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ph \/ ps ) ) -> ( ph \/ ps ) )
Theorem	pm4.44 768	Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph \/ ( ph /\ ps ) ) )
Theorem	pm4.56 769	Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- ( ( -. ph /\ -. ps ) <-> -. ( ph \/ ps ) )
Theorem	oranim 770	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 771	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 772	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 773	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph /\ ( ph \/ ps ) ) )
Theorem	pm3.48 774	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 775	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 776	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( ps \/ th ) -> ( ch \/ th ) ) )
Theorem	orim2d 777	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )
Theorem	orim2 778	Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)
|- ( ( ps -> ch ) -> ( ( ph \/ ps ) -> ( ph \/ ch ) ) )
Theorem	orbi2d 779	Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )
Theorem	orbi1d 780	Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )
Theorem	orbi1 781	Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph <-> ps ) -> ( ( ph \/ ch ) <-> ( ps \/ ch ) ) )
Theorem	orbi12d 782	Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   =>    |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )
Theorem	pm5.61 783	Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
|- ( ( ( ph \/ ps ) /\ -. ps ) <-> ( ph /\ -. ps ) )
Theorem	jaoian 784	Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( th /\ ps ) -> ch )   =>    |- ( ( ( ph \/ th ) /\ ps ) -> ch )
Theorem	jao1i 785	Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.)
|- ( ps -> ( ch -> ph ) )   =>    |- ( ( ph \/ ps ) -> ( ch -> ph ) )
Theorem	jaodan 786	Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ th ) -> ch )   =>    |- ( ( ph /\ ( ps \/ th ) ) -> ch )
Theorem	mpjaodan 787	Eliminate a disjunction in a deduction. A translation of natural deduction rule \/ E ( \/ elimination). (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ th ) -> ch )   &    |- ( ph -> ( ps \/ th ) )   =>    |- ( ph -> ch )
Theorem	pm4.77 788	Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ps -> ph ) /\ ( ch -> ph ) ) <-> ( ( ps \/ ch ) -> ph ) )
Theorem	pm2.63 789	Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ps ) -> ( ( -. ph \/ ps ) -> ps ) )
Theorem	pm2.64 790	Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ps ) -> ( ( ph \/ -. ps ) -> ph ) )
Theorem	pm5.53 791	Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ( ph \/ ps ) \/ ch ) -> th ) <-> ( ( ( ph -> th ) /\ ( ps -> th ) ) /\ ( ch -> th ) ) )
Theorem	pm2.38 792	Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
|- ( ( ps -> ch ) -> ( ( ps \/ ph ) -> ( ch \/ ph ) ) )
Theorem	pm2.36 793	Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
|- ( ( ps -> ch ) -> ( ( ph \/ ps ) -> ( ch \/ ph ) ) )
Theorem	pm2.37 794	Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
|- ( ( ps -> ch ) -> ( ( ps \/ ph ) -> ( ph \/ ch ) ) )
Theorem	pm2.73 795	Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ( ph \/ ps ) \/ ch ) -> ( ps \/ ch ) ) )
Theorem	pm2.74 796	Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.)
|- ( ( ps -> ph ) -> ( ( ( ph \/ ps ) \/ ch ) -> ( ph \/ ch ) ) )
Theorem	pm2.76 797	Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ( ph \/ ( ps -> ch ) ) -> ( ( ph \/ ps ) -> ( ph \/ ch ) ) )
Theorem	pm2.75 798	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 799	Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.)
|- ( ( ph \/ ps ) -> ( ( -. ps \/ ch ) -> ( ph \/ ch ) ) )
Theorem	pm2.81 800	Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
|- ( ( ps -> ( ch -> th ) ) -> ( ( ph \/ ps ) -> ( ( ph \/ ch ) -> ( ph \/ th ) ) ) )