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	pm5.21im 701	Two propositions are equivalent if they are both false. Closed form of 2false 706. 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 702	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 703	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 704	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 705	Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.)
|- ph   =>    |- ( -. ps <-> ( ps <-> -. ph ) )
Theorem	2false 706	Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- -. ph   &    |- -. ps   =>    |- ( ph <-> ps )
Theorem	2falsed 707	Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.)
|- ( ph -> -. ps )   &    |- ( ph -> -. ch )   =>    |- ( ph -> ( ps <-> ch ) )
Theorem	pm5.21ni 708	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 709	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 710	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 711	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 712	Theorem *4.8 of [WhiteheadRussell] p. 122. This one holds for all propositions, but compare with pm4.81dc 913 which requires a decidability condition. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> -. ph ) <-> -. ph )
1.2.6  Logical disjunction
Syntax	wo 713	Extend wff definition to include disjunction ('or').
wff ( ph \/ ps )
Axiom	ax-io 714	Definition of 'or'. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias jaob 715 instead. (New usage is discouraged.)
|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
Theorem	jaob 715	Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121. Alias of ax-io 714. (Contributed by NM, 30-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
Theorem	olc 716	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 717	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 718	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 719	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 720	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 721	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 722	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 723	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 724	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 725	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 726	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 902. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- ( ( -. ph \/ ps ) -> ( ph -> ps ) )
Theorem	pm2.53 727	Theorem *2.53 of [WhiteheadRussell] p. 107. This holds intuitionistically, although its converse does not (see pm2.54dc 896). (Contributed by NM, 3-Jan-2005.) (Revised by NM, 31-Jan-2015.)
|- ( ( ph \/ ps ) -> ( -. ph -> ps ) )
Theorem	ori 728	Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph \/ ps )   =>    |- ( -. ph -> ps )
Theorem	ord 729	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 730	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 731	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 732	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 733	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 734	Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)
|- ( ph -> ( ps \/ ch ) )   =>    |- ( ph -> ( ch \/ ps ) )
Theorem	orcoms 735	Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012.)
|- ( ( ph \/ ps ) -> ch )   =>    |- ( ( ps \/ ph ) -> ch )
Theorem	orci 736	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>    |- ( ph \/ ps )
Theorem	olci 737	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>    |- ( ps \/ ph )
Theorem	orcd 738	Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
|- ( ph -> ps )   =>    |- ( ph -> ( ps \/ ch ) )
Theorem	olcd 739	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 740	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 741	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 742	Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
|- ( ph -> ( ph \/ ph ) )
Theorem	pm2.45 743	Theorem *2.45 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> -. ph )
Theorem	pm2.46 744	Theorem *2.46 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> -. ps )
Theorem	pm2.47 745	Theorem *2.47 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> ( -. ph \/ ps ) )
Theorem	pm2.48 746	Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> ( ph \/ -. ps ) )
Theorem	pm2.49 747	Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph \/ ps ) -> ( -. ph \/ -. ps ) )
Theorem	pm2.67 748	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 749	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 750	A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.)
|- ( ph -> ( ps <-> ( -. ph \/ ps ) ) )
Theorem	biorfi 751	A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.)
|- -. ph   =>    |- ( ps <-> ( ps \/ ph ) )
Theorem	pm2.621 752	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 753	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 754	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 755	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 756	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 757	Negated disjunction in terms of conjunction. This version of DeMorgan's law is a biconditional for all propositions (not just decidable ones), unlike oranim 786, anordc 962, or ianordc 904. 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 758	Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 904. The converse holds for decidable propositions, as seen at pm3.13dc 965. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ( -. ph \/ -. ps ) -> -. ( ph /\ ps ) )
Theorem	pm3.1 759	Theorem *3.1 of [WhiteheadRussell] p. 111. The converse holds for decidable propositions, as seen at anordc 962. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ( ph /\ ps ) -> -. ( -. ph \/ -. ps ) )
Theorem	jao 760	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 761	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 762	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 763	Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph \/ ph ) )
Theorem	orim12i 764	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 765	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
|- ( ph -> ps )   =>    |- ( ( ph \/ ch ) -> ( ps \/ ch ) )
Theorem	orim2i 766	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
|- ( ph -> ps )   =>    |- ( ( ch \/ ph ) -> ( ch \/ ps ) )
Theorem	orbi2i 767	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 768	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 769	Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph \/ ch ) <-> ( ps \/ th ) )
Theorem	pm1.5 770	Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ps \/ ch ) ) -> ( ps \/ ( ph \/ ch ) ) )
Theorem	or12 771	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 772	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 773	Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ps \/ ch ) ) -> ( ( ph \/ ps ) \/ ch ) )
Theorem	pm2.32 774	Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph \/ ps ) \/ ch ) -> ( ph \/ ( ps \/ ch ) ) )
Theorem	or32 775	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 776	Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
|- ( ( ( ph \/ ps ) \/ ( ch \/ th ) ) <-> ( ( ph \/ ch ) \/ ( ps \/ th ) ) )
Theorem	or42 777	Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
|- ( ( ( ph \/ ps ) \/ ( ch \/ th ) ) <-> ( ( ph \/ ch ) \/ ( th \/ ps ) ) )
Theorem	orordi 778	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
|- ( ( ph \/ ( ps \/ ch ) ) <-> ( ( ph \/ ps ) \/ ( ph \/ ch ) ) )
Theorem	orordir 779	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
|- ( ( ( ph \/ ps ) \/ ch ) <-> ( ( ph \/ ch ) \/ ( ps \/ ch ) ) )
Theorem	pm2.3 780	Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ps \/ ch ) ) -> ( ph \/ ( ch \/ ps ) ) )
Theorem	pm2.41 781	Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( ( ps \/ ( ph \/ ps ) ) -> ( ph \/ ps ) )
Theorem	pm2.42 782	Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( ( -. ph \/ ( ph -> ps ) ) -> ( ph -> ps ) )
Theorem	pm2.4 783	Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph \/ ( ph \/ ps ) ) -> ( ph \/ ps ) )
Theorem	pm4.44 784	Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph \/ ( ph /\ ps ) ) )
Theorem	pm4.56 785	Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- ( ( -. ph /\ -. ps ) <-> -. ( ph \/ ps ) )
Theorem	oranim 786	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 787	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 788	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 789	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph /\ ( ph \/ ps ) ) )
Theorem	pm3.48 790	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 791	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 792	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( ps \/ th ) -> ( ch \/ th ) ) )
Theorem	orim2d 793	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )
Theorem	orim2 794	Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)
|- ( ( ps -> ch ) -> ( ( ph \/ ps ) -> ( ph \/ ch ) ) )
Theorem	orbi2d 795	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 796	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 797	Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph <-> ps ) -> ( ( ph \/ ch ) <-> ( ps \/ ch ) ) )
Theorem	orbi12d 798	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 799	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 800	Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( th /\ ps ) -> ch )   =>    |- ( ( ( ph \/ th ) /\ ps ) -> ch )