Home | Metamath
Proof Explorer Theorem List (p. 10 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pm2.07 901 | Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 → (𝜑 ∨ 𝜑)) | ||
Theorem | pm1.2 902 | Axiom *1.2 of [WhiteheadRussell] p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜑) → 𝜑) | ||
Theorem | oridm 903 | 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 904 | Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 ↔ (𝜑 ∨ 𝜑)) | ||
Theorem | pm2.4 905 | Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓)) | ||
Theorem | pm2.41 906 | Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓)) | ||
Theorem | orim12i 907 | Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)) | ||
Theorem | orim1i 908 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒)) | ||
Theorem | orim2i 909 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) | ||
Theorem | orim12dALT 910 | Alternate proof of orim12d 963 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 911 | 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 912 | Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) | ||
Theorem | orbi12i 913 | Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) | ||
Theorem | orbi2d 914 | Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) | ||
Theorem | orbi1d 915 | Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) | ||
Theorem | orbi1 916 | Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))) | ||
Theorem | orbi12d 917 | Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) | ||
Theorem | pm1.5 918 | Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜓 ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | or12 919 | Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ (𝜓 ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | orass 920 | 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 921 | Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜓) ∨ 𝜒)) | ||
Theorem | pm2.32 922 | Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | pm2.3 923 | Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜑 ∨ (𝜒 ∨ 𝜓))) | ||
Theorem | or32 924 | A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜓)) | ||
Theorem | or4 925 | Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜃))) | ||
Theorem | or42 926 | Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜃 ∨ 𝜓))) | ||
Theorem | orordi 927 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | orordir 928 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | orimdi 929 | Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.) |
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.76 930 | Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.85 931 | Theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)) → (𝜑 ∨ (𝜓 → 𝜒))) | ||
Theorem | pm2.75 932 | Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.) |
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm4.78 933 | 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 934 | A disjunction with a true formula is equivalent to that true formula. (Contributed by NM, 23-May-1999.) |
⊢ (𝜑 → (𝜑 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | biorf 935 | 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 936 | A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.) |
⊢ (𝜑 → (𝜓 ↔ (¬ 𝜑 ∨ 𝜓))) | ||
Theorem | biorfi 937 | 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 938 | 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 939 | Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜑 ∨ 𝜓) → 𝜓)) | ||
Theorem | pm2.64 940 | Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ ¬ 𝜓) → 𝜑)) | ||
Theorem | pm2.42 941 | Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∨ (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | pm5.11g 942 | A general instance of Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜒)) | ||
Theorem | pm5.11 943 | Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜓)) | ||
Theorem | pm5.12 944 | Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜑 → ¬ 𝜓)) | ||
Theorem | pm5.14 945 | Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜒)) | ||
Theorem | pm5.13 946 | Theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜑)) | ||
Theorem | pm5.55 947 | Theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 20-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∨ 𝜓) ↔ 𝜓)) | ||
Theorem | pm4.72 948 | 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 949 | Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
⊢ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∨ 𝜒))) | ||
Theorem | oibabs 950 | Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) |
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) ↔ (𝜑 ↔ 𝜓)) | ||
Theorem | orbidi 951 | 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 952 | Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 951. (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 963 versus orim12dALT 910). These theorems are mostly grouped at the beginning of this section. The family of theorems starting with animorl 976 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 953 and related theorems. | ||
Theorem | jaao 953 | Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∨ 𝜏) → 𝜒)) | ||
Theorem | jaoa 954 | Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜒)) ⇒ ⊢ ((𝜑 ∨ 𝜃) → ((𝜓 ∧ 𝜏) → 𝜒)) | ||
Theorem | jaoian 955 | Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜃 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒) | ||
Theorem | jaodan 956 | Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) | ||
Theorem | mpjaodan 957 | Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 29145. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) & ⊢ (𝜑 → (𝜓 ∨ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm3.44 958 | Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) → ((𝜓 ∨ 𝜒) → 𝜑)) | ||
Theorem | jao 959 | 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 960 | 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 961 | Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) ↔ ((𝜓 ∨ 𝜒) → 𝜑)) | ||
Theorem | pm3.48 962 | Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))) | ||
Theorem | orim12d 963 | Disjoin antecedents and consequents in a deduction. See orim12dALT 910 for a proof which does not depend on df-an 397. (Contributed by NM, 10-May-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) | ||
Theorem | orim1d 964 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃))) | ||
Theorem | orim2d 965 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) | ||
Theorem | orim2 966 | Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.38 967 | Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜒 ∨ 𝜑))) | ||
Theorem | pm2.36 968 | Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜒 ∨ 𝜑))) | ||
Theorem | pm2.37 969 | Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.81 970 | Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 → (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜓) → ((𝜑 ∨ 𝜒) → (𝜑 ∨ 𝜃)))) | ||
Theorem | pm2.8 971 | Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.73 972 | Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜓 ∨ 𝜒))) | ||
Theorem | pm2.74 973 | Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ ((𝜓 → 𝜑) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.82 974 | Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (((𝜑 ∨ ¬ 𝜒) ∨ 𝜃) → ((𝜑 ∨ 𝜓) ∨ 𝜃))) | ||
Theorem | pm4.39 975 | Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ↔ 𝜒) ∧ (𝜓 ↔ 𝜃)) → ((𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜃))) | ||
Theorem | animorl 976 | Conjunction implies disjunction with one common formula (1/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∨ 𝜒)) | ||
Theorem | animorr 977 | Conjunction implies disjunction with one common formula (2/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜓)) | ||
Theorem | animorlr 978 | Conjunction implies disjunction with one common formula (3/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜑)) | ||
Theorem | animorrl 979 | Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒)) | ||
Theorem | ianor 980 | 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 981 | 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 982 | 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 983 | Theorem *4.52 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.) |
⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (¬ 𝜑 ∨ 𝜓)) | ||
Theorem | pm4.53 984 | Theorem *4.53 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∧ ¬ 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) | ||
Theorem | pm4.54 985 | Theorem *4.54 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.) |
⊢ ((¬ 𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm4.55 986 | Theorem *4.55 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm4.56 987 | Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓)) | ||
Theorem | oran 988 | 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 989 | Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 ∧ ¬ 𝜓) ↔ (𝜑 ∨ 𝜓)) | ||
Theorem | pm3.1 990 | Theorem *3.1 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∧ 𝜓) → ¬ (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm3.11 991 | Theorem *3.11 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓)) | ||
Theorem | pm3.12 992 | Theorem *3.12 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)) | ||
Theorem | pm3.13 993 | Theorem *3.13 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm3.14 994 | Theorem *3.14 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) | ||
Theorem | pm4.44 995 | Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 ↔ (𝜑 ∨ (𝜑 ∧ 𝜓))) | ||
Theorem | pm4.45 996 | Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 ↔ (𝜑 ∧ (𝜑 ∨ 𝜓))) | ||
Theorem | orabs 997 | 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 998 | 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 999 | Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.) |
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ 𝜓) ↔ (𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm5.6 1000 | Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.) |
⊢ (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |