P. 9 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 801-900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exbiri 801	Inference form of exbir 39638. This proof is exbiriVD 40023 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
Theorem	pm2.61ian 802	Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	pm2.61dan 803	Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61ddan 804	Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	pm2.61dda 805	Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ ¬ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mtand 806	A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm2.65da 807	Deduction for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	condan 808	Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ 𝜒)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	biadan 809	An implication is equivalent to the equivalence of some implied equivalence and some other equivalence involving a conjunction. A utility lemma as illustrated in biadanii 813 and elelb 33456. (Contributed by BJ, 4-Mar-2023.) (Proof shortened by Wolf Lammen, 8-Mar-2023.)
⊢ ((𝜑 → 𝜓) ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒))))
Theorem	biadanOLD 810	Obsolete version of biadan 809 as of 8-Mar-2023. (Contributed by BJ, 4-Mar-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒))))
Theorem	biadani 811	Inference associated with biadan 809. (Contributed by BJ, 4-Mar-2023.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	biadaniALT 812	Alternate proof of biadani 811 not using biadan 809. (Contributed by BJ, 4-Mar-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	biadanii 813	Inference associated with biadani 811. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
Theorem	biadan2OLD 814	Obsolete proof of biadanii 813 as of 4-Mar-2023. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
Theorem	pm5.1 815	Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123. (Contributed by NM, 21-May-1994.)
⊢ ((𝜑 ∧ 𝜓) → (𝜑 ↔ 𝜓))
Theorem	pm5.21 816	Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124. (Contributed by NM, 21-May-1994.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → (𝜑 ↔ 𝜓))
Theorem	pm5.35 817	Theorem *5.35 of [WhiteheadRussell] p. 125. Closed form of 2thd 257. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ↔ 𝜒)))
Theorem	abai 818	Introduce one conjunct as an antecedent to the other. "abai" stands for "and, biconditional, and, implication". (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (𝜑 → 𝜓)))
Theorem	pm4.45im 819	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)
⊢ (𝜑 ↔ (𝜑 ∧ (𝜓 → 𝜑)))
Theorem	nan 820	Theorem to move a conjunct in and out of a negation. (Contributed by NM, 9-Nov-2003.)
⊢ ((𝜑 → ¬ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) → ¬ 𝜒))
Theorem	pm5.31 821	Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜒 ∧ (𝜑 → 𝜓)) → (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	pm5.31r 822	Variant of pm5.31 821. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ ((𝜒 ∧ (𝜑 → 𝜓)) → (𝜑 → (𝜒 ∧ 𝜓)))
Theorem	pm4.15 823	Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
⊢ (((𝜑 ∧ 𝜓) → ¬ 𝜒) ↔ ((𝜓 ∧ 𝜒) → ¬ 𝜑))
Theorem	pm5.36 824	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∧ (𝜑 ↔ 𝜓)) ↔ (𝜓 ∧ (𝜑 ↔ 𝜓)))
Theorem	annotanannot 825	A conjunction with a negated conjunction. (Contributed by AV, 8-Mar-2022.) (Proof shortened by Wolf Lammen, 1-Apr-2022.)
⊢ ((𝜑 ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	pm5.33 826	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∧ (𝜓 → 𝜒)) ↔ (𝜑 ∧ ((𝜑 ∧ 𝜓) → 𝜒)))
Theorem	syl12anc 827	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl21anc 828	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl22anc 829	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl1111anc 830	Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1442 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	mpsyl4anc 831	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜃 → 𝜂)
Theorem	pm4.87 832	Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Eric Schmidt, 26-Oct-2006.)
⊢ (((((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) ∧ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))) ∧ ((𝜓 → (𝜑 → 𝜒)) ↔ ((𝜓 ∧ 𝜑) → 𝜒)))
Theorem	bimsc1 833	Removal of conjunct from one side of an equivalence. (Contributed by NM, 21-Jun-1993.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 ↔ (𝜓 ∧ 𝜑))) → (𝜒 ↔ 𝜑))
Theorem	a2and 834	Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
⊢ (𝜑 → ((𝜓 ∧ 𝜌) → (𝜏 → 𝜃)))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜌) → 𝜒))    ⇒   ⊢ (𝜑 → (((𝜓 ∧ 𝜒) → 𝜏) → ((𝜓 ∧ 𝜌) → 𝜃)))
Theorem	animpimp2impd 835	Deduction deriving nested implications from conjunctions. (Contributed by AV, 21-Aug-2022.)
⊢ ((𝜓 ∧ 𝜑) → (𝜒 → (𝜃 → 𝜂)))    &   ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜃)) → (𝜂 → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → (𝜃 → 𝜏))))
1.2.7  Logical disjunction This section defines disjunction of two formulas, denoted by infix "∨ " and read "or". It is defined in terms of implication and negation, which is possible in classical logic (but not in intuitionistic logic: see iset.mm). This section contains only theorems proved without df-an 387 (theorems that are proved using df-an 387 are deferred to the next section). Basic theorems that help simplifying and applying disjunction are olc 857, orc 856, and orcom 859. As mentioned in the "note on definitions" in the section comment for logical equivalence, all theorems in this and the previous section can be stated in terms of implication and negation only. Additionally, in classical logic (but not in intuitionistic logic: see iset.mm), it is also possible to translate conjunction into disjunction and conversely via the De Morgan law anor 968: conjunction and disjunction are dual connectives. Either is sufficient to develop all propositional calculus of the logic (together with implication and negation). In practice, conjunction is more efficient, its big advantage being the possibility to use it to group antecedents in a convenient way, using imp 397 and ex 403 as noted in the previous section. An illustration of the conservativity of df-an 387 is given by orim12dALT 898, which is an alternate proof of orim12d 950 not using df-an 387.
Syntax	wo 836	Extend wff definition to include disjunction ("or").
wff (𝜑 ∨ 𝜓)
Definition	df-or 837	Define disjunction (logical "or"). Definition of [Margaris] p. 49. When the left operand, right operand, or both are true, the result is true; when both sides are false, the result is false. For example, it is true that (2 = 3 ∨ 4 = 4) (ex-or 27853). After we define the constant true ⊤ (df-tru 1605) and the constant false ⊥ (df-fal 1615), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1639), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1640), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1641), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1642). Contrast with ∧ (df-an 387), → (wi 4), ⊼ (df-nan 1558), and ⊻ (df-xor 1583). (Contributed by NM, 27-Dec-1992.)
⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
Theorem	pm4.64 838	Theorem *4.64 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))
Theorem	pm4.66 839	Theorem *4.66 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))
Theorem	pm2.53 840	Theorem *2.53 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))
Theorem	pm2.54 841	Theorem *2.54 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜓) → (𝜑 ∨ 𝜓))
Theorem	imor 842	Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.)
⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
Theorem	imori 843	Infer disjunction from implication. (Contributed by NM, 12-Mar-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜑 ∨ 𝜓)
Theorem	imorri 844	Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (¬ 𝜑 ∨ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm4.62 845	Theorem *4.62 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	jaoi 846	Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → 𝜓)
Theorem	jao1i 847	Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.)
⊢ (𝜓 → (𝜒 → 𝜑))    ⇒   ⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑))
Theorem	jaod 848	Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
Theorem	mpjaod 849	Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	ori 850	Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.)
⊢ (𝜑 ∨ 𝜓)    ⇒   ⊢ (¬ 𝜑 → 𝜓)
Theorem	orri 851	Infer disjunction from implication. (Contributed by NM, 11-Jun-1994.)
⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ∨ 𝜓)
Theorem	orrd 852	Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ∨ 𝜒))
Theorem	ord 853	Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
Theorem	orci 854	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (𝜑 ∨ 𝜓)
Theorem	olci 855	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ∨ 𝜑)
Theorem	orc 856	Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)
⊢ (𝜑 → (𝜑 ∨ 𝜓))
Theorem	olc 857	Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.)
⊢ (𝜑 → (𝜓 ∨ 𝜑))
Theorem	pm1.4 858	Axiom *1.4 of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑))
Theorem	orcom 859	Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.)
⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))
Theorem	orcomd 860	Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ∨ 𝜓))
Theorem	orcoms 861	Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜓 ∨ 𝜑) → 𝜒)
Theorem	orcd 862	Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 27835. (Contributed by NM, 20-Sep-2007.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ∨ 𝜒))
Theorem	olcd 863	Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 27835. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ∨ 𝜓))
Theorem	orcs 864	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 17) -type inference in a proof. (Contributed by NM, 21-Jun-1994.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	olcs 865	Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	mtord 866	A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm3.2ni 867	Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)
⊢ ¬ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ ¬ (𝜑 ∨ 𝜓)
Theorem	pm2.45 868	Theorem *2.45 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
Theorem	pm2.46 869	Theorem *2.46 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
Theorem	pm2.47 870	Theorem *2.47 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∨ 𝜓))
Theorem	pm2.48 871	Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ∨ ¬ 𝜓))
Theorem	pm2.49 872	Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	norbi 873	If neither of two propositions is true, then these propositions are equivalent. (Contributed by BJ, 26-Apr-2019.)
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓))
Theorem	nbior 874	If two propositions are not equivalent, then at least one is true. (Contributed by BJ, 19-Apr-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
⊢ (¬ (𝜑 ↔ 𝜓) → (𝜑 ∨ 𝜓))
Theorem	orel1 875	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	pm2.25 876	Theorem *2.25 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ∨ ((𝜑 ∨ 𝜓) → 𝜓))
Theorem	orel2 877	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	pm2.67-2 878	Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ∨ 𝜒) → 𝜓) → (𝜑 → 𝜓))
Theorem	pm2.67 879	Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) → 𝜓) → (𝜑 → 𝜓))
Theorem	curryax 880	A non-intuitionistic positive statement, sometimes called a paradox of material implication. Sometimes called Curry's axiom. Similar to exmid 881 but positive. For another non-intuitionistic positive statement, see peirce 194. (Contributed by BJ, 4-Apr-2021.)
⊢ (𝜑 ∨ (𝜑 → 𝜓))
Theorem	exmid 881	Law of excluded middle, also called the principle of tertium non datur. Theorem *2.11 of [WhiteheadRussell] p. 101. It says that something is either true or not true; there are no in-between values of truth. This is an essential distinction of our classical logic and is not a theorem of intuitionistic logic. In intuitionistic logic, if this statement is true for some 𝜑, then 𝜑 is decidable. (Contributed by NM, 29-Dec-1992.)
⊢ (𝜑 ∨ ¬ 𝜑)
Theorem	exmidd 882	Law of excluded middle in a context. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓))
Theorem	pm2.1 883	Theorem *2.1 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
⊢ (¬ 𝜑 ∨ 𝜑)
Theorem	pm2.13 884	Theorem *2.13 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ∨ ¬ ¬ ¬ 𝜑)
Theorem	pm2.621 885	Theorem *2.621 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) → ((𝜑 ∨ 𝜓) → 𝜓))
Theorem	pm2.62 886	Theorem *2.62 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.)
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 → 𝜓) → 𝜓))
Theorem	pm2.68 887	Theorem *2.68 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) → 𝜓) → (𝜑 ∨ 𝜓))
Theorem	dfor2 888	Logical 'or' expressed in terms of implication only. Theorem *5.25 of [WhiteheadRussell] p. 124. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Wolf Lammen, 20-Oct-2012.)
⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 → 𝜓) → 𝜓))
Theorem	pm2.07 889	Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → (𝜑 ∨ 𝜑))
Theorem	pm1.2 890	Axiom *1.2 of [WhiteheadRussell] p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜑) → 𝜑)
Theorem	oridm 891	Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.)
⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)
Theorem	pm4.25 892	Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∨ 𝜑))
Theorem	pm2.4 893	Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
Theorem	pm2.41 894	Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
Theorem	orim12i 895	Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))
Theorem	orim1i 896	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒))
Theorem	orim2i 897	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))
Theorem	orim12dALT 898	Alternate proof of orim12d 950 which does not depend on df-an 387. This is an illustration of the conservativity of definitions (definitions do not permit to prove additional theorems whose statements do not contain the defined symbol). (Contributed by Wolf Lammen, 8-Aug-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
Theorem	orbi2i 899	Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
Theorem	orbi1i 900	Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))