Home | Metamath
Proof Explorer Theorem List (p. 10 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pm2.41 901 | Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓)) | ||
Theorem | orim12i 902 | Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)) | ||
Theorem | orim1i 903 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒)) | ||
Theorem | orim2i 904 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) | ||
Theorem | orim12dALT 905 | Alternate proof of orim12d 958 which does not depend on df-an 397. 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 906 | 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 907 | Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) | ||
Theorem | orbi12i 908 | Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) | ||
Theorem | orbi2d 909 | Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) | ||
Theorem | orbi1d 910 | Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) | ||
Theorem | orbi1 911 | Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))) | ||
Theorem | orbi12d 912 | Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) | ||
Theorem | pm1.5 913 | Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜓 ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | or12 914 | Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ (𝜓 ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | orass 915 | 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 916 | Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜓) ∨ 𝜒)) | ||
Theorem | pm2.32 917 | Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | pm2.3 918 | Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜑 ∨ (𝜒 ∨ 𝜓))) | ||
Theorem | or32 919 | A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜓)) | ||
Theorem | or4 920 | Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜃))) | ||
Theorem | or42 921 | Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜃 ∨ 𝜓))) | ||
Theorem | orordi 922 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | orordir 923 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | orimdi 924 | Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.) |
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.76 925 | Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.85 926 | Theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)) → (𝜑 ∨ (𝜓 → 𝜒))) | ||
Theorem | pm2.75 927 | Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.) |
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm4.78 928 | Implication distributes over disjunction. Theorem *4.78 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
⊢ (((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∨ 𝜒))) | ||
Theorem | biort 929 | A wff disjoined with truth is true. (Contributed by NM, 23-May-1999.) |
⊢ (𝜑 → (𝜑 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | biorf 930 | 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 931 | A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.) |
⊢ (𝜑 → (𝜓 ↔ (¬ 𝜑 ∨ 𝜓))) | ||
Theorem | biorfi 932 | A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 16-Jul-2021.) |
⊢ ¬ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑)) | ||
Theorem | pm2.26 933 | Theorem *2.26 of [WhiteheadRussell] p. 104. See pm2.27 42. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
⊢ (¬ 𝜑 ∨ ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | pm2.63 934 | Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜑 ∨ 𝜓) → 𝜓)) | ||
Theorem | pm2.64 935 | Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ ¬ 𝜓) → 𝜑)) | ||
Theorem | pm2.42 936 | Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∨ (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | pm5.11g 937 | A general instance of Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜒)) | ||
Theorem | pm5.11 938 | Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜓)) | ||
Theorem | pm5.12 939 | Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜑 → ¬ 𝜓)) | ||
Theorem | pm5.14 940 | Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜒)) | ||
Theorem | pm5.13 941 | Theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜑)) | ||
Theorem | pm5.55 942 | Theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 20-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∨ 𝜓) ↔ 𝜓)) | ||
Theorem | pm4.72 943 | Implication in terms of biconditional and disjunction. Theorem *4.72 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jan-2013.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | imimorb 944 | Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
⊢ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∨ 𝜒))) | ||
Theorem | oibabs 945 | Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) |
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) ↔ (𝜑 ↔ 𝜓)) | ||
Theorem | orbidi 946 | Disjunction distributes over the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384. (Contributed by NM, 8-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Feb-2013.) |
⊢ ((𝜑 ∨ (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ 𝜒))) | ||
Theorem | pm5.7 947 | Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 946. (Contributed by Roy F. Longton, 21-Jun-2005.) |
⊢ (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓))) | ||
This section gathers theorems of propositional calculus which use (either in their statement or proof) mixed connectives (at least conjunction and disjunction). As noted in the "note on definitions" in the section comment for logical equivalence, some theorem statements may contain for instance only conjunction or only disjunction, but both definitions are used in their proofs to make them shorter (this is exemplified in orim12d 958 versus orim12dALT 905). These theorems are mostly grouped at the beginning of this section. The family of theorems starting with animorl 971 focus on the relation between conjunction and disjunction and can be seen as the starting point of mixed connectives in statements. This sectioning is not rigorously true, since for instance the section begins with jaao 948 and related theorems. | ||
Theorem | jaao 948 | Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∨ 𝜏) → 𝜒)) | ||
Theorem | jaoa 949 | Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜒)) ⇒ ⊢ ((𝜑 ∨ 𝜃) → ((𝜓 ∧ 𝜏) → 𝜒)) | ||
Theorem | jaoian 950 | Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜃 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒) | ||
Theorem | jaodan 951 | Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) | ||
Theorem | mpjaodan 952 | Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 28110. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) & ⊢ (𝜑 → (𝜓 ∨ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm3.44 953 | Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) → ((𝜓 ∨ 𝜒) → 𝜑)) | ||
Theorem | jao 954 | 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 | jaob 955 | Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 9-Dec-2012.) |
⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓))) | ||
Theorem | pm4.77 956 | Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) ↔ ((𝜓 ∨ 𝜒) → 𝜑)) | ||
Theorem | pm3.48 957 | Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))) | ||
Theorem | orim12d 958 | Disjoin antecedents and consequents in a deduction. See orim12dALT 905 for a proof which does not depend on df-an 397. (Contributed by NM, 10-May-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) | ||
Theorem | orim1d 959 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃))) | ||
Theorem | orim2d 960 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) | ||
Theorem | orim2 961 | Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.38 962 | Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜒 ∨ 𝜑))) | ||
Theorem | pm2.36 963 | Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜒 ∨ 𝜑))) | ||
Theorem | pm2.37 964 | Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.81 965 | Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 → (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜓) → ((𝜑 ∨ 𝜒) → (𝜑 ∨ 𝜃)))) | ||
Theorem | pm2.8 966 | Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.73 967 | Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜓 ∨ 𝜒))) | ||
Theorem | pm2.74 968 | Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ ((𝜓 → 𝜑) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.82 969 | Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (((𝜑 ∨ ¬ 𝜒) ∨ 𝜃) → ((𝜑 ∨ 𝜓) ∨ 𝜃))) | ||
Theorem | pm4.39 970 | Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ↔ 𝜒) ∧ (𝜓 ↔ 𝜃)) → ((𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜃))) | ||
Theorem | animorl 971 | Conjunction implies disjunction with one common formula (1/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∨ 𝜒)) | ||
Theorem | animorr 972 | Conjunction implies disjunction with one common formula (2/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜓)) | ||
Theorem | animorlr 973 | Conjunction implies disjunction with one common formula (3/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜑)) | ||
Theorem | animorrl 974 | Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒)) | ||
Theorem | ianor 975 | Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | anor 976 | Conjunction in terms of disjunction (De Morgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Nov-2012.) |
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | ioran 977 | Negated disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm4.52 978 | Theorem *4.52 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.) |
⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (¬ 𝜑 ∨ 𝜓)) | ||
Theorem | pm4.53 979 | Theorem *4.53 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∧ ¬ 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) | ||
Theorem | pm4.54 980 | Theorem *4.54 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.) |
⊢ ((¬ 𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm4.55 981 | Theorem *4.55 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm4.56 982 | Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓)) | ||
Theorem | oran 983 | Disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ ((𝜑 ∨ 𝜓) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm4.57 984 | Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 ∧ ¬ 𝜓) ↔ (𝜑 ∨ 𝜓)) | ||
Theorem | pm3.1 985 | Theorem *3.1 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∧ 𝜓) → ¬ (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm3.11 986 | Theorem *3.11 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓)) | ||
Theorem | pm3.12 987 | Theorem *3.12 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)) | ||
Theorem | pm3.13 988 | Theorem *3.13 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm3.14 989 | Theorem *3.14 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) | ||
Theorem | pm4.44 990 | Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 ↔ (𝜑 ∨ (𝜑 ∧ 𝜓))) | ||
Theorem | pm4.45 991 | Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 ↔ (𝜑 ∧ (𝜑 ∨ 𝜓))) | ||
Theorem | orabs 992 | Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 28-Feb-2014.) |
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ 𝜑)) | ||
Theorem | oranabs 993 | Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.) |
⊢ (((𝜑 ∨ ¬ 𝜓) ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | pm5.61 994 | Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.) |
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ 𝜓) ↔ (𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm5.6 995 | Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.) |
⊢ (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒))) | ||
Theorem | orcanai 996 | Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) | ||
Theorem | pm4.79 997 | Theorem *4.79 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2013.) |
⊢ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜑)) ↔ ((𝜓 ∧ 𝜒) → 𝜑)) | ||
Theorem | pm5.53 998 | Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((((𝜑 ∨ 𝜓) ∨ 𝜒) → 𝜃) ↔ (((𝜑 → 𝜃) ∧ (𝜓 → 𝜃)) ∧ (𝜒 → 𝜃))) | ||
Theorem | ordi 999 | Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 28-Nov-2013.) |
⊢ ((𝜑 ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒))) | ||
Theorem | ordir 1000 | Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |