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	simp-7l 801	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜑)
Theorem	simp-7r 802	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Theorem	simp-8l 803	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜑)
Theorem	simp-8r 804	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Theorem	simp-9l 805	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜑)
Theorem	simp-9r 806	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)
Theorem	simp-10l 807	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜑)
Theorem	simp-10r 808	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓)
Theorem	simp-11l 809	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜑)
Theorem	simp-11r 810	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓)
Theorem	pm2.01da 811	Deduction based on reductio ad absurdum. See pm2.01 190. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm2.18da 812	Deduction based on reductio ad absurdum. See pm2.18 129. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	impbida 813	Deduce an equivalence from two implications. Variant of impbid 215. (Contributed by NM, 17-Feb-2007.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	pm5.21nd 814	Eliminate an antecedent implied by each side of a biconditional. Variant of pm5.21ndd 382. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ (𝜃 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	pm3.35 815	Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. Variant of pm2.27 43. (Contributed by NM, 14-Dec-2002.)
⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)
Theorem	pm5.74da 816	Distribution of implication over biconditional (deduction form). Variant of pm5.74d 276. (Contributed by NM, 4-May-2007.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
Theorem	bitr 817	Theorem *4.22 of [WhiteheadRussell] p. 117. bitri 278 in closed form. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜓 ↔ 𝜒)) → (𝜑 ↔ 𝜒))
Theorem	biantr 818	A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜓)) → (𝜑 ↔ 𝜒))
Theorem	pm4.14 819	Theorem *4.14 of [WhiteheadRussell] p. 117. Related to con34b 319. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Oct-2012.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓))
Theorem	pm3.37 820	Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Oct-2012.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) → ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓))
Theorem	anim12 821	Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 621. 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 822	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.)
⊢ ((𝜑 ∧ 𝜓) → (𝜑 → 𝜓))
Theorem	exbiri 823	Inference form of exbir 45229. This proof is exbiriVD 45603 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
Theorem	pm2.61ian 824	Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	pm2.61dan 825	Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61ddan 826	Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	pm2.61dda 827	Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ ¬ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mtand 828	A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm2.65da 829	Deduction for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	condan 830	Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ 𝜒)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	biadan 831	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 834 and elelb 37573. (Contributed by BJ, 4-Mar-2023.) (Proof shortened by Wolf Lammen, 8-Mar-2023.)
⊢ ((𝜑 → 𝜓) ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒))))
Theorem	biadani 832	Inference associated with biadan 831. (Contributed by BJ, 4-Mar-2023.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	biadaniALT 833	Alternate proof of biadani 832 not using biadan 831. (Contributed by BJ, 4-Mar-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	biadanii 834	Inference associated with biadani 832. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
Theorem	biadanid 835	Deduction associated with biadani 832. Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
Theorem	pm5.1 836	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 837	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 838	Theorem *5.35 of [WhiteheadRussell] p. 125. Closed form of 2thd 268. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ↔ 𝜒)))
Theorem	abai 839	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	abab 840	Introduce one conjunct as equivalent to the other. "abab" stands for "and, biconditional, and, biconditional". (Contributed by Wolf Lammen, 4-Jun-2026.)
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (𝜑 ↔ 𝜓)))
Theorem	pm4.45im 841	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)
⊢ (𝜑 ↔ (𝜑 ∧ (𝜓 → 𝜑)))
Theorem	impimprbi 842	An implication and its reverse are equivalent exactly when both operands are equivalent. The right hand side resembles that of dfbi2 480, but ↔ is a weaker operator than ∧. Note that an implication and its reverse can never be simultaneously false, because of pm2.521 177. (Contributed by Wolf Lammen, 18-Dec-2023.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ↔ (𝜓 → 𝜑)))
Theorem	nan 843	Theorem to move a conjunct in and out of a negation. (Contributed by NM, 9-Nov-2003.)
⊢ ((𝜑 → ¬ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) → ¬ 𝜒))
Theorem	pm5.31 844	Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜒 ∧ (𝜑 → 𝜓)) → (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	pm5.31r 845	Variant of pm5.31 844. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ ((𝜒 ∧ (𝜑 → 𝜓)) → (𝜑 → (𝜒 ∧ 𝜓)))
Theorem	pm4.15 846	Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
⊢ (((𝜑 ∧ 𝜓) → ¬ 𝜒) ↔ ((𝜓 ∧ 𝜒) → ¬ 𝜑))
Theorem	pm5.36 847	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∧ (𝜑 ↔ 𝜓)) ↔ (𝜓 ∧ (𝜑 ↔ 𝜓)))
Theorem	annotanannot 848	A conjunction with a negated conjunction. (Contributed by AV, 8-Mar-2022.) (Proof shortened by Wolf Lammen, 1-Apr-2022.)
⊢ ((𝜑 ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	pm5.33 849	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∧ (𝜓 → 𝜒)) ↔ (𝜑 ∧ ((𝜑 ∧ 𝜓) → 𝜒)))
Theorem	syl12anc 850	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl21anc 851	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl22anc 852	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	bibiad 853	Eliminate an hypothesis 𝜃 in a biconditional. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	syl1111anc 854	Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1401 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syldbl2 855	Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ ((𝜑 ∧ 𝜓) → (𝜓 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mpsyl4anc 856	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜃 → 𝜂)
Theorem	pm4.87 857	Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Eric Schmidt, 26-Oct-2006.)
⊢ (((((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) ∧ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))) ∧ ((𝜓 → (𝜑 → 𝜒)) ↔ ((𝜓 ∧ 𝜑) → 𝜒)))
Theorem	bimsc1 858	Removal of conjunct from one side of an equivalence. (Contributed by NM, 21-Jun-1993.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 ↔ (𝜓 ∧ 𝜑))) → (𝜒 ↔ 𝜑))
Theorem	a2and 859	Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
⊢ (𝜑 → ((𝜓 ∧ 𝜌) → (𝜏 → 𝜃)))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜌) → 𝜒))    ⇒   ⊢ (𝜑 → (((𝜓 ∧ 𝜒) → 𝜏) → ((𝜓 ∧ 𝜌) → 𝜃)))
Theorem	animpimp2impd 860	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 402 (theorems that are proved using df-an 402 are deferred to the next section). Basic theorems that help simplifying and applying disjunction are olc 882, orc 881, and orcom 884. 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 998: 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 412 and ex 418 as noted in the previous section. An illustration of the conservativity of df-an 402 is given by orim12dALT 925, which is an alternate proof of orim12d 979 not using df-an 402.
Syntax	wo 861	Extend wff definition to include disjunction ("or").
wff (𝜑 ∨ 𝜓)
Definition	df-or 862	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 30809). After we define the constant true ⊤ (df-tru 1573) and the constant false ⊥ (df-fal 1583), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1607), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1608), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1609), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1610). Contrast with ∧ (df-an 402), → (wi 4), ⊼ (df-nan 1522), and ⊻ (df-xor 1542). (Contributed by NM, 27-Dec-1992.)
⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
Theorem	pm4.64 863	Theorem *4.64 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))
Theorem	pm4.66 864	Theorem *4.66 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))
Theorem	pm2.53 865	Theorem *2.53 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))
Theorem	pm2.54 866	Theorem *2.54 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜓) → (𝜑 ∨ 𝜓))
Theorem	imor 867	Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.)
⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
Theorem	imori 868	Infer disjunction from implication. (Contributed by NM, 12-Mar-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜑 ∨ 𝜓)
Theorem	imorri 869	Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (¬ 𝜑 ∨ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm4.62 870	Theorem *4.62 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	jaoi 871	Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → 𝜓)
Theorem	jao1i 872	Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.)
⊢ (𝜓 → (𝜒 → 𝜑))    ⇒   ⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑))
Theorem	jaod 873	Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
Theorem	mpjaod 874	Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	ori 875	Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.)
⊢ (𝜑 ∨ 𝜓)    ⇒   ⊢ (¬ 𝜑 → 𝜓)
Theorem	orri 876	Infer disjunction from implication. (Contributed by NM, 11-Jun-1994.)
⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ∨ 𝜓)
Theorem	orrd 877	Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ∨ 𝜒))
Theorem	ord 878	Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
Theorem	orci 879	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (𝜑 ∨ 𝜓)
Theorem	olci 880	Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ∨ 𝜑)
Theorem	orc 881	Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)
⊢ (𝜑 → (𝜑 ∨ 𝜓))
Theorem	olc 882	Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.)
⊢ (𝜑 → (𝜓 ∨ 𝜑))
Theorem	pm1.4 883	Axiom *1.4 of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑))
Theorem	orcom 884	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 885	Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ∨ 𝜓))
Theorem	orcoms 886	Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜓 ∨ 𝜑) → 𝜒)
Theorem	orcd 887	Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30791. (Contributed by NM, 20-Sep-2007.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ∨ 𝜒))
Theorem	olcd 888	Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 30791. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ∨ 𝜓))
Theorem	orcs 889	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 18) -type inference in a proof. (Contributed by NM, 21-Jun-1994.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	olcs 890	Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	olcnd 891	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	orcnd 892	A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mtord 893	A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm3.2ni 894	Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)
⊢ ¬ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ ¬ (𝜑 ∨ 𝜓)
Theorem	pm2.45 895	Theorem *2.45 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
Theorem	pm2.46 896	Theorem *2.46 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
Theorem	pm2.47 897	Theorem *2.47 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∨ 𝜓))
Theorem	pm2.48 898	Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ∨ ¬ 𝜓))
Theorem	pm2.49 899	Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	norbi 900	If neither of two propositions is true, then these propositions are equivalent. (Contributed by BJ, 26-Apr-2019.)
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓))