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