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	olc 701	Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
⊢ (𝜑 → (𝜓 ∨ 𝜑))
Theorem	orc 702	Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
⊢ (𝜑 → (𝜑 ∨ 𝜓))
Theorem	pm2.67-2 703	Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
⊢ (((𝜑 ∨ 𝜒) → 𝜓) → (𝜑 → 𝜓))
Theorem	oibabs 704	Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) ↔ (𝜑 ↔ 𝜓))
Theorem	pm3.44 705	Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) → ((𝜓 ∨ 𝜒) → 𝜑))
Theorem	jaoi 706	Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → 𝜓)
Theorem	jaod 707	Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
Theorem	mpjaod 708	Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	jaao 709	Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∨ 𝜏) → 𝜒))
Theorem	jaoa 710	Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    ⇒   ⊢ ((𝜑 ∨ 𝜃) → ((𝜓 ∧ 𝜏) → 𝜒))
Theorem	imorr 711	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 887. (Contributed by Jim Kingdon, 21-Jul-2018.)
⊢ ((¬ 𝜑 ∨ 𝜓) → (𝜑 → 𝜓))
Theorem	pm2.53 712	Theorem *2.53 of [WhiteheadRussell] p. 107. This holds intuitionistically, although its converse does not (see pm2.54dc 881). (Contributed by NM, 3-Jan-2005.) (Revised by NM, 31-Jan-2015.)
⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))
Theorem	ori 713	Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
⊢ (𝜑 ∨ 𝜓)    ⇒   ⊢ (¬ 𝜑 → 𝜓)
Theorem	ord 714	Deduce implication from disjunction. (Contributed by NM, 18-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
Theorem	orel1 715	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.)
⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))
Theorem	orel2 716	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.)
⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓))
Theorem	pm1.4 717	Axiom *1.4 of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 15-Nov-2012.)
⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑))
Theorem	orcom 718	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.)
⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))
Theorem	orcomd 719	Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ∨ 𝜓))
Theorem	orcoms 720	Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜓 ∨ 𝜑) → 𝜒)
Theorem	orci 721	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
⊢ 𝜑    ⇒   ⊢ (𝜑 ∨ 𝜓)
Theorem	olci 722	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ∨ 𝜑)
Theorem	orcd 723	Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ∨ 𝜒))
Theorem	olcd 724	Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ∨ 𝜓))
Theorem	orcs 725	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.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	olcs 726	Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	pm2.07 727	Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → (𝜑 ∨ 𝜑))
Theorem	pm2.45 728	Theorem *2.45 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
Theorem	pm2.46 729	Theorem *2.46 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
Theorem	pm2.47 730	Theorem *2.47 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∨ 𝜓))
Theorem	pm2.48 731	Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ∨ ¬ 𝜓))
Theorem	pm2.49 732	Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	pm2.67 733	Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
⊢ (((𝜑 ∨ 𝜓) → 𝜓) → (𝜑 → 𝜓))
Theorem	biorf 734	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.)
⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))
Theorem	biortn 735	A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.)
⊢ (𝜑 → (𝜓 ↔ (¬ 𝜑 ∨ 𝜓)))
Theorem	biorfi 736	A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.)
⊢ ¬ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))
Theorem	pm2.621 737	Theorem *2.621 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 13-Dec-2013.)
⊢ ((𝜑 → 𝜓) → ((𝜑 ∨ 𝜓) → 𝜓))
Theorem	pm2.62 738	Theorem *2.62 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.)
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 → 𝜓) → 𝜓))
Theorem	imorri 739	Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by Mario Carneiro, 31-Jan-2015.)
⊢ (¬ 𝜑 ∨ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm4.52im 740	One direction of theorem *4.52 of [WhiteheadRussell] p. 120. The converse also holds in classical logic. (Contributed by Jim Kingdon, 27-Jul-2018.)
⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ (¬ 𝜑 ∨ 𝜓))
Theorem	pm4.53r 741	One direction of theorem *4.53 of [WhiteheadRussell] p. 120. The converse also holds in classical logic. (Contributed by Jim Kingdon, 27-Jul-2018.)
⊢ ((¬ 𝜑 ∨ 𝜓) → ¬ (𝜑 ∧ ¬ 𝜓))
Theorem	ioran 742	Negated disjunction in terms of conjunction. This version of DeMorgan's law is a biconditional for all propositions (not just decidable ones), unlike oranim 771, anordc 946, or ianordc 889. Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	pm3.14 743	Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 889. The converse holds for decidable propositions, as seen at pm3.13dc 949. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
Theorem	pm3.1 744	Theorem *3.1 of [WhiteheadRussell] p. 111. The converse holds for decidable propositions, as seen at anordc 946. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
⊢ ((𝜑 ∧ 𝜓) → ¬ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	jao 745	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.)
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜓) → ((𝜑 ∨ 𝜒) → 𝜓)))
Theorem	pm1.2 746	Axiom *1.2 (Taut) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 10-Mar-2013.)
⊢ ((𝜑 ∨ 𝜑) → 𝜑)
Theorem	oridm 747	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.)
⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)
Theorem	pm4.25 748	Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∨ 𝜑))
Theorem	orim12i 749	Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))
Theorem	orim1i 750	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒))
Theorem	orim2i 751	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))
Theorem	orbi2i 752	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.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
Theorem	orbi1i 753	Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))
Theorem	orbi12i 754	Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))
Theorem	pm1.5 755	Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜓 ∨ (𝜑 ∨ 𝜒)))
Theorem	or12 756	Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ (𝜓 ∨ (𝜑 ∨ 𝜒)))
Theorem	orass 757	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.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	pm2.31 758	Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜓) ∨ 𝜒))
Theorem	pm2.32 759	Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	or32 760	A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜓))
Theorem	or4 761	Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜃)))
Theorem	or42 762	Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜃 ∨ 𝜓)))
Theorem	orordi 763	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜒)))
Theorem	orordir 764	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜒)))
Theorem	pm2.3 765	Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜑 ∨ (𝜒 ∨ 𝜓)))
Theorem	pm2.41 766	Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
Theorem	pm2.42 767	Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ (𝜑 → 𝜓)) → (𝜑 → 𝜓))
Theorem	pm2.4 768	Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
Theorem	pm4.44 769	Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∨ (𝜑 ∧ 𝜓)))
Theorem	pm4.56 770	Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))
Theorem	oranim 771	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.)
⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	pm4.78i 772	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.)
⊢ (((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∨ 𝜒)))
Theorem	mtord 773	A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.) (Revised by Mario Carneiro, 31-Jan-2015.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm4.45 774	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∧ (𝜑 ∨ 𝜓)))
Theorem	pm3.48 775	Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) (Revised by NM, 1-Dec-2012.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)))
Theorem	orim12d 776	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
Theorem	orim1d 777	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃)))
Theorem	orim2d 778	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))
Theorem	orim2 779	Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))
Theorem	orbi2d 780	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.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))
Theorem	orbi1d 781	Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
Theorem	orbi1 782	Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)))
Theorem	orbi12d 783	Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
Theorem	pm5.61 784	Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ 𝜓) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	jaoian 785	Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒)
Theorem	jao1i 786	Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.)
⊢ (𝜓 → (𝜒 → 𝜑))    ⇒   ⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑))
Theorem	jaodan 787	Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
Theorem	mpjaodan 788	Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm4.77 789	Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) ↔ ((𝜓 ∨ 𝜒) → 𝜑))
Theorem	pm2.63 790	Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜑 ∨ 𝜓) → 𝜓))
Theorem	pm2.64 791	Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ ¬ 𝜓) → 𝜑))
Theorem	pm5.53 792	Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((((𝜑 ∨ 𝜓) ∨ 𝜒) → 𝜃) ↔ (((𝜑 → 𝜃) ∧ (𝜓 → 𝜃)) ∧ (𝜒 → 𝜃)))
Theorem	pm2.38 793	Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜒 ∨ 𝜑)))
Theorem	pm2.36 794	Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜒 ∨ 𝜑)))
Theorem	pm2.37 795	Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜒)))
Theorem	pm2.73 796	Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜓 ∨ 𝜒)))
Theorem	pm2.74 797	Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.)
⊢ ((𝜓 → 𝜑) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ 𝜒)))
Theorem	pm2.76 798	Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))
Theorem	pm2.75 799	Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.)
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒)))
Theorem	pm2.8 800	Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.)
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒)))