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	bitr 801	Theorem *4.22 of [WhiteheadRussell] p. 117. bitri 274 in closed form. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜓 ↔ 𝜒)) → (𝜑 ↔ 𝜒))
Theorem	biantr 802	A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜓)) → (𝜑 ↔ 𝜒))
Theorem	pm4.14 803	Theorem *4.14 of [WhiteheadRussell] p. 117. Related to con34b 315. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Oct-2012.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓))
Theorem	pm3.37 804	Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Oct-2012.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) → ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓))
Theorem	anim12 805	Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 608. Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it praeclarum theorema (splendid theorem). (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃)))
Theorem	pm3.4 806	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.)
⊢ ((𝜑 ∧ 𝜓) → (𝜑 → 𝜓))
Theorem	exbiri 807	Inference form of exbir 41987. This proof is exbiriVD 42363 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
Theorem	pm2.61ian 808	Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	pm2.61dan 809	Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61ddan 810	Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	pm2.61dda 811	Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ ¬ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mtand 812	A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm2.65da 813	Deduction for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	condan 814	Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ 𝜒)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	biadan 815	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 818 and elelb 35009. (Contributed by BJ, 4-Mar-2023.) (Proof shortened by Wolf Lammen, 8-Mar-2023.)
⊢ ((𝜑 → 𝜓) ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒))))
Theorem	biadani 816	Inference associated with biadan 815. (Contributed by BJ, 4-Mar-2023.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	biadaniALT 817	Alternate proof of biadani 816 not using biadan 815. (Contributed by BJ, 4-Mar-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	biadanii 818	Inference associated with biadani 816. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
Theorem	biadanid 819	Deduction associated with biadani 816. Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
Theorem	pm5.1 820	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 821	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 822	Theorem *5.35 of [WhiteheadRussell] p. 125. Closed form of 2thd 264. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ↔ 𝜒)))
Theorem	abai 823	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 824	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)
⊢ (𝜑 ↔ (𝜑 ∧ (𝜓 → 𝜑)))
Theorem	impimprbi 825	An implication and its reverse are equivalent exactly when both operands are equivalent. The right hand side resembles that of dfbi2 474, but ↔ is a weaker operator than ∧. Note that an implication and its reverse can never be simultaneously false, because of pm2.521 176. (Contributed by Wolf Lammen, 18-Dec-2023.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ↔ (𝜓 → 𝜑)))
Theorem	nan 826	Theorem to move a conjunct in and out of a negation. (Contributed by NM, 9-Nov-2003.)
⊢ ((𝜑 → ¬ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) → ¬ 𝜒))
Theorem	pm5.31 827	Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜒 ∧ (𝜑 → 𝜓)) → (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	pm5.31r 828	Variant of pm5.31 827. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ ((𝜒 ∧ (𝜑 → 𝜓)) → (𝜑 → (𝜒 ∧ 𝜓)))
Theorem	pm4.15 829	Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
⊢ (((𝜑 ∧ 𝜓) → ¬ 𝜒) ↔ ((𝜓 ∧ 𝜒) → ¬ 𝜑))
Theorem	pm5.36 830	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∧ (𝜑 ↔ 𝜓)) ↔ (𝜓 ∧ (𝜑 ↔ 𝜓)))
Theorem	annotanannot 831	A conjunction with a negated conjunction. (Contributed by AV, 8-Mar-2022.) (Proof shortened by Wolf Lammen, 1-Apr-2022.)
⊢ ((𝜑 ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	pm5.33 832	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∧ (𝜓 → 𝜒)) ↔ (𝜑 ∧ ((𝜑 ∧ 𝜓) → 𝜒)))
Theorem	syl12anc 833	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl21anc 834	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl22anc 835	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl1111anc 836	Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1372 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syldbl2 837	Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ ((𝜑 ∧ 𝜓) → (𝜓 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mpsyl4anc 838	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜃 → 𝜂)
Theorem	pm4.87 839	Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Eric Schmidt, 26-Oct-2006.)
⊢ (((((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) ∧ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))) ∧ ((𝜓 → (𝜑 → 𝜒)) ↔ ((𝜓 ∧ 𝜑) → 𝜒)))
Theorem	bimsc1 840	Removal of conjunct from one side of an equivalence. (Contributed by NM, 21-Jun-1993.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 ↔ (𝜓 ∧ 𝜑))) → (𝜒 ↔ 𝜑))
Theorem	a2and 841	Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
⊢ (𝜑 → ((𝜓 ∧ 𝜌) → (𝜏 → 𝜃)))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜌) → 𝜒))    ⇒   ⊢ (𝜑 → (((𝜓 ∧ 𝜒) → 𝜏) → ((𝜓 ∧ 𝜌) → 𝜃)))
Theorem	animpimp2impd 842	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 396 (theorems that are proved using df-an 396 are deferred to the next section). Basic theorems that help simplifying and applying disjunction are olc 864, orc 863, and orcom 866. 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 979: 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 406 and ex 412 as noted in the previous section. An illustration of the conservativity of df-an 396 is given by orim12dALT 908, which is an alternate proof of orim12d 961 not using df-an 396.
Syntax	wo 843	Extend wff definition to include disjunction ("or").
wff (𝜑 ∨ 𝜓)
Definition	df-or 844	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 28686). After we define the constant true ⊤ (df-tru 1542) and the constant false ⊥ (df-fal 1552), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1576), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1577), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1578), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1579). Contrast with ∧ (df-an 396), → (wi 4), ⊼ (df-nan 1484), and ⊻ (df-xor 1504). (Contributed by NM, 27-Dec-1992.)
⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
Theorem	pm4.64 845	Theorem *4.64 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))
Theorem	pm4.66 846	Theorem *4.66 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))
Theorem	pm2.53 847	Theorem *2.53 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))
Theorem	pm2.54 848	Theorem *2.54 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜓) → (𝜑 ∨ 𝜓))
Theorem	imor 849	Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.)
⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
Theorem	imori 850	Infer disjunction from implication. (Contributed by NM, 12-Mar-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜑 ∨ 𝜓)
Theorem	imorri 851	Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (¬ 𝜑 ∨ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm4.62 852	Theorem *4.62 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	jaoi 853	Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → 𝜓)
Theorem	jao1i 854	Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.)
⊢ (𝜓 → (𝜒 → 𝜑))    ⇒   ⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑))
Theorem	jaod 855	Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
Theorem	mpjaod 856	Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	ori 857	Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.)
⊢ (𝜑 ∨ 𝜓)    ⇒   ⊢ (¬ 𝜑 → 𝜓)
Theorem	orri 858	Infer disjunction from implication. (Contributed by NM, 11-Jun-1994.)
⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ∨ 𝜓)
Theorem	orrd 859	Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ∨ 𝜒))
Theorem	ord 860	Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
Theorem	orci 861	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (𝜑 ∨ 𝜓)
Theorem	olci 862	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ∨ 𝜑)
Theorem	orc 863	Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)
⊢ (𝜑 → (𝜑 ∨ 𝜓))
Theorem	olc 864	Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.)
⊢ (𝜑 → (𝜓 ∨ 𝜑))
Theorem	pm1.4 865	Axiom *1.4 of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑))
Theorem	orcom 866	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 867	Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ∨ 𝜓))
Theorem	orcoms 868	Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜓 ∨ 𝜑) → 𝜒)
Theorem	orcd 869	Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 28668. (Contributed by NM, 20-Sep-2007.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ∨ 𝜒))
Theorem	olcd 870	Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 28668. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ∨ 𝜓))
Theorem	orcs 871	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 872	Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	olcnd 873	A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2024.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	unitreslOLD 874	Obsolete version of olcnd 873 as of 13-Apr-2024. (Contributed by Giovanni Mascellani, 15-Sep-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	orcnd 875	A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mtord 876	A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm3.2ni 877	Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)
⊢ ¬ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ ¬ (𝜑 ∨ 𝜓)
Theorem	pm2.45 878	Theorem *2.45 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
Theorem	pm2.46 879	Theorem *2.46 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
Theorem	pm2.47 880	Theorem *2.47 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∨ 𝜓))
Theorem	pm2.48 881	Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ∨ ¬ 𝜓))
Theorem	pm2.49 882	Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	norbi 883	If neither of two propositions is true, then these propositions are equivalent. (Contributed by BJ, 26-Apr-2019.)
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓))
Theorem	nbior 884	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 885	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 886	Theorem *2.25 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ∨ ((𝜑 ∨ 𝜓) → 𝜓))
Theorem	orel2 887	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 888	Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ∨ 𝜒) → 𝜓) → (𝜑 → 𝜓))
Theorem	pm2.67 889	Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) → 𝜓) → (𝜑 → 𝜓))
Theorem	curryax 890	A non-intuitionistic positive statement, sometimes called a paradox of material implication. Sometimes called Curry's axiom. Similar to exmid 891 (obtained by substituting ⊥ for 𝜓) but positive. For another non-intuitionistic positive statement, see peirce 201. (Contributed by BJ, 4-Apr-2021.)
⊢ (𝜑 ∨ (𝜑 → 𝜓))
Theorem	exmid 891	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 892	Law of excluded middle in a context. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓))
Theorem	pm2.1 893	Theorem *2.1 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
⊢ (¬ 𝜑 ∨ 𝜑)
Theorem	pm2.13 894	Theorem *2.13 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ∨ ¬ ¬ ¬ 𝜑)
Theorem	pm2.621 895	Theorem *2.621 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) → ((𝜑 ∨ 𝜓) → 𝜓))
Theorem	pm2.62 896	Theorem *2.62 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.)
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 → 𝜓) → 𝜓))
Theorem	pm2.68 897	Theorem *2.68 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) → 𝜓) → (𝜑 ∨ 𝜓))
Theorem	dfor2 898	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 899	Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → (𝜑 ∨ 𝜑))
Theorem	pm1.2 900	Axiom *1.2 of [WhiteheadRussell] p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜑) → 𝜑)