Home | Metamath
Proof Explorer Theorem List (p. 10 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oranabs 901 | Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.) |
⊢ (((𝜑 ∨ ¬ 𝜓) ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | pm5.1 902 | 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 903 | Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124. (Contributed by NM, 21-May-1994.) |
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → (𝜑 ↔ 𝜓)) | ||
Theorem | norbi 904 | If neither of two propositions is true, then these propositions are equivalent. (Contributed by BJ, 26-Apr-2019.) |
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) | ||
Theorem | nbior 905 | 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 | pm3.43 906 | Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒))) | ||
Theorem | jcab 907 | Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.) |
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))) | ||
Theorem | ordi 908 | 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 909 | Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))) | ||
Theorem | pm4.76 910 | Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒))) | ||
Theorem | andi 911 | Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | ||
Theorem | andir 912 | Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
Theorem | orddi 913 | Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)) ↔ (((𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜃)) ∧ ((𝜓 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)))) | ||
Theorem | anddi 914 | Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)) ∨ ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))) | ||
Theorem | pm4.39 915 | Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ↔ 𝜒) ∧ (𝜓 ↔ 𝜃)) → ((𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜃))) | ||
Theorem | pm4.38 916 | Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ↔ 𝜒) ∧ (𝜓 ↔ 𝜃)) → ((𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃))) | ||
Theorem | bi2anan9 917 | Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) | ||
Theorem | bi2anan9r 918 | Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) | ||
Theorem | bi2bian9 919 | Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ↔ 𝜏) ↔ (𝜒 ↔ 𝜂))) | ||
Theorem | pm4.72 920 | 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 921 | Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
⊢ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∨ 𝜒))) | ||
Theorem | pm5.33 922 | Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∧ (𝜓 → 𝜒)) ↔ (𝜑 ∧ ((𝜑 ∧ 𝜓) → 𝜒))) | ||
Theorem | pm5.36 923 | Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∧ (𝜑 ↔ 𝜓)) ↔ (𝜓 ∧ (𝜑 ↔ 𝜓))) | ||
Theorem | bianabs 924 | Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.) |
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | oibabs 925 | Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) |
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) ↔ (𝜑 ↔ 𝜓)) | ||
Theorem | pm3.24 926 | Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ ¬ (𝜑 ∧ ¬ 𝜑) | ||
Theorem | pm2.26 927 | Theorem *2.26 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
⊢ (¬ 𝜑 ∨ ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | pm5.11 928 | Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜓)) | ||
Theorem | pm5.12 929 | Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜑 → ¬ 𝜓)) | ||
Theorem | pm5.14 930 | Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜒)) | ||
Theorem | pm5.13 931 | Theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜑)) | ||
Theorem | pm5.17 932 | Theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | pm5.15 933 | Theorem *5.15 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 15-Oct-2013.) |
⊢ ((𝜑 ↔ 𝜓) ∨ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | pm5.16 934 | Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 17-Oct-2013.) |
⊢ ¬ ((𝜑 ↔ 𝜓) ∧ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | xor 935 | Two ways to express "exclusive or." Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.) |
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑))) | ||
Theorem | nbi2 936 | Two ways to express "exclusive or." (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.) |
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) | ||
Theorem | xordi 937 | Conjunction distributes over exclusive-or, using ¬ (𝜑 ↔ 𝜓) to express exclusive-or. This is one way to interpret the distributive law of multiplication over addition in modulo 2 arithmetic. This is not necessarily true in intuitionistic logic, though anxordi 1479 does hold in it. (Contributed by NM, 3-Oct-2008.) |
⊢ ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) | ||
Theorem | biort 938 | A wff disjoined with truth is true. (Contributed by NM, 23-May-1999.) |
⊢ (𝜑 → (𝜑 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | pm5.55 939 | Theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 20-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∨ 𝜓) ↔ 𝜓)) | ||
Theorem | ornld 940 | Selecting one statement from a disjunction if one of the disjuncted statements is false. (Contributed by AV, 6-Sep-2018.) (Proof shortened by AV, 13-Oct-2018.) (Proof shortened by Wolf Lammen, 19-Jan-2020.) |
⊢ (𝜑 → (((𝜑 → (𝜃 ∨ 𝜏)) ∧ ¬ 𝜃) → 𝜏)) | ||
Theorem | pm5.21nd 941 | Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜃) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) & ⊢ (𝜃 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | pm5.35 942 | Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ↔ 𝜒))) | ||
Theorem | pm5.54 943 | Theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 7-Nov-2013.) |
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∧ 𝜓) ↔ 𝜓)) | ||
Theorem | baib 944 | Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜑 ↔ 𝜒)) | ||
Theorem | baibr 945 | Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜒 ↔ 𝜑)) | ||
Theorem | rbaibr 946 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜓 ↔ 𝜑)) | ||
Theorem | rbaib 947 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜑 ↔ 𝜓)) | ||
Theorem | baibd 948 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃)) | ||
Theorem | rbaibd 949 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) | ||
Theorem | pm5.44 950 | Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) ↔ (𝜑 → (𝜓 ∧ 𝜒)))) | ||
Theorem | pm5.6 951 | Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.) |
⊢ (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒))) | ||
Theorem | orcanai 952 | Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) | ||
Theorem | mpbiran 953 | Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) |
⊢ 𝜓 & ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | mpbiran2 954 | Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) |
⊢ 𝜒 & ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | mpbir2an 955 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) |
⊢ 𝜓 & ⊢ 𝜒 & ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ 𝜑 | ||
Theorem | mpbi2and 956 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | mpbir2and 957 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → 𝜓) | ||
This subsection gathers miscellaneous theorems of propositional calculus, including proofs by cases and other theorems with negated wffs. | ||
Theorem | pm5.62 958 | Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm5.63 959 | Theorem *5.63 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 25-Dec-2012.) |
⊢ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓))) | ||
Theorem | intnan 960 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜓 ∧ 𝜑) | ||
Theorem | intnanr 961 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜑 ∧ 𝜓) | ||
Theorem | intnand 962 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓)) | ||
Theorem | intnanrd 963 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) | ||
Theorem | niabn 964 | Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑)) | ||
Theorem | ninba 965 | Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓))) | ||
Theorem | bianfi 966 | A wff conjoined with falsehood is false. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.) |
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) | ||
Theorem | bianfd 967 | A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | pm4.43 968 | Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.) |
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓))) | ||
Theorem | pm4.82 969 | Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑) | ||
Theorem | pm4.83 970 | Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓) | ||
Theorem | pclem6 971 | Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.) |
⊢ ((𝜑 ↔ (𝜓 ∧ ¬ 𝜑)) → ¬ 𝜓) | ||
Theorem | biantr 972 | A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜓)) → (𝜑 ↔ 𝜒)) | ||
Theorem | orbidi 973 | 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 | biluk 974 | Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96. (Contributed by NM, 10-Jan-2005.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒))) | ||
Theorem | pm5.7 975 | Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 973. (Contributed by Roy F. Longton, 21-Jun-2005.) |
⊢ (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓))) | ||
Theorem | bigolden 976 | Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.) |
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | pm5.71 977 | Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.) |
⊢ ((𝜓 → ¬ 𝜒) → (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ 𝜒))) | ||
Theorem | pm5.75 978 | Theorem *5.75 of [WhiteheadRussell] p. 126. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2012.) (Proof shortened by Kyle Wyonch, 12-Feb-2021.) |
⊢ (((𝜒 → ¬ 𝜓) ∧ (𝜑 ↔ (𝜓 ∨ 𝜒))) → ((𝜑 ∧ ¬ 𝜓) ↔ 𝜒)) | ||
Theorem | pm5.75OLD 979 | Obsolete proof of pm5.75 978 as of 12-Feb-2021. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (((𝜒 → ¬ 𝜓) ∧ (𝜑 ↔ (𝜓 ∨ 𝜒))) → ((𝜑 ∧ ¬ 𝜓) ↔ 𝜒)) | ||
Theorem | bimsc1 980 | Removal of conjunct from one side of an equivalence. (Contributed by NM, 21-Jun-1993.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜒 ↔ (𝜓 ∧ 𝜑))) → (𝜒 ↔ 𝜑)) | ||
Theorem | ecase2d 981 | Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Dec-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) & ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜃)) & ⊢ (𝜑 → (𝜏 ∨ (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | ecase3 982 | Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜓 → 𝜒) & ⊢ (¬ (𝜑 ∨ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | ecase 983 | Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.) |
⊢ (¬ 𝜑 → 𝜒) & ⊢ (¬ 𝜓 → 𝜒) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | ecase3d 984 | Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (¬ (𝜓 ∨ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | ecased 985 | Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜃)) & ⊢ (𝜑 → (¬ 𝜒 → 𝜃)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | ecase3ad 986 | Deduction for elimination by cases. (Contributed by NM, 24-May-2013.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → ((¬ 𝜓 ∧ ¬ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | ccase 987 | Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜏) & ⊢ ((𝜒 ∧ 𝜓) → 𝜏) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) | ||
Theorem | ccased 988 | Deduction for combining cases. (Contributed by NM, 9-May-2004.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂)) | ||
Theorem | ccase2 989 | Inference for combining cases. (Contributed by NM, 29-Jul-1999.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜏) & ⊢ (𝜒 → 𝜏) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) | ||
Theorem | 4cases 990 | Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) & ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | 4casesdan 991 | Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) & ⊢ ((𝜑 ∧ (𝜓 ∧ ¬ 𝜒)) → 𝜃) & ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ 𝜒)) → 𝜃) & ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | cases 992 | Case disjunction according to the value of 𝜑. (Contributed by NM, 25-Apr-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜓 ↔ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜃))) | ||
Theorem | cases2 993 | Case disjunction according to the value of 𝜑. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 2-Jan-2020.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | dfbi3 994 | An alternate definition of the biconditional. Theorem *5.23 of [WhiteheadRussell] p. 124. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) (Proof shortened by NM, 29-Oct-2021.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓))) | ||
Theorem | dfbi3OLD 995 | Obsolete proof of dfbi3 994 as of 29-Oct-2021. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓))) | ||
Theorem | pm5.24 996 | Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑))) | ||
Theorem | 4exmid 997 | The disjunction of the four possible combinations of two wffs and their negations is always true. A four-way excluded middle (see exmid 431). (Contributed by David Abernethy, 28-Jan-2014.) (Proof shortened by NM, 29-Oct-2021.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ∨ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑))) | ||
Theorem | 4exmidOLD 998 | Obsolete proof of 4exmid 997 as of 29-Oct-2021. (Contributed by David Abernethy, 28-Jan-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ∨ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑))) | ||
Theorem | consensus 999 | The consensus theorem. This theorem and its dual (with ∨ and ∧ interchanged) are commonly used in computer logic design to eliminate redundant terms from Boolean expressions. Specifically, we prove that the term (𝜓 ∧ 𝜒) on the left-hand side is redundant. (Contributed by NM, 16-May-2003.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 20-Jan-2013.) |
⊢ ((((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) | ||
Theorem | dedlem0a 1000 | Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
⊢ (𝜑 → (𝜓 ↔ ((𝜒 → 𝜑) → (𝜓 ∧ 𝜑)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |