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