Home | Metamath
Proof Explorer Theorem List (p. 11 of 465) | < 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-29276) |
Hilbert Space Explorer
(29277-30799) |
Users' Mathboxes
(30800-46482) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pm4.79 1001 | Theorem *4.79 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2013.) |
⊢ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜑)) ↔ ((𝜓 ∧ 𝜒) → 𝜑)) | ||
Theorem | pm5.53 1002 | Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((((𝜑 ∨ 𝜓) ∨ 𝜒) → 𝜃) ↔ (((𝜑 → 𝜃) ∧ (𝜓 → 𝜃)) ∧ (𝜒 → 𝜃))) | ||
Theorem | ordi 1003 | 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 1004 | Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))) | ||
Theorem | andi 1005 | 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 1006 | Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
Theorem | orddi 1007 | Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)) ↔ (((𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜃)) ∧ ((𝜓 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)))) | ||
Theorem | anddi 1008 | Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)) ∨ ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))) | ||
Theorem | pm5.17 1009 | Theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | pm5.15 1010 | Theorem *5.15 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 15-Oct-2013.) |
⊢ ((𝜑 ↔ 𝜓) ∨ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | pm5.16 1011 | Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 17-Oct-2013.) |
⊢ ¬ ((𝜑 ↔ 𝜓) ∧ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | xor 1012 | Two ways to express exclusive disjunction (df-xor 1507). Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.) |
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑))) | ||
Theorem | nbi2 1013 | Two ways to express "exclusive or". (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.) |
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) | ||
Theorem | xordi 1014 | 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 1523 does hold in it. (Contributed by NM, 3-Oct-2008.) |
⊢ ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) | ||
Theorem | pm5.54 1015 | Theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 7-Nov-2013.) |
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∧ 𝜓) ↔ 𝜓)) | ||
Theorem | pm5.62 1016 | Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm5.63 1017 | Theorem *5.63 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 25-Dec-2012.) |
⊢ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓))) | ||
Theorem | niabn 1018 | Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑)) | ||
Theorem | ninba 1019 | Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓))) | ||
Theorem | pm4.43 1020 | Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.) |
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓))) | ||
Theorem | pm4.82 1021 | Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑) | ||
Theorem | pm4.83 1022 | Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓) | ||
Theorem | pclem6 1023 | Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.) |
⊢ ((𝜑 ↔ (𝜓 ∧ ¬ 𝜑)) → ¬ 𝜓) | ||
Theorem | bigolden 1024 | Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.) |
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | pm5.71 1025 | Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.) |
⊢ ((𝜓 → ¬ 𝜒) → (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ 𝜒))) | ||
Theorem | pm5.75 1026 | 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 | ecase2d 1027 | Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Sep-2024.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) & ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜃)) & ⊢ (𝜑 → (𝜏 ∨ (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | ecase2dOLD 1028 | Obsolete version of ecase2d 1027 as of 19-Sep-2024. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Dec-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) & ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜃)) & ⊢ (𝜑 → (𝜏 ∨ (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | ecase3 1029 | Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜓 → 𝜒) & ⊢ (¬ (𝜑 ∨ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | ecase 1030 | Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.) |
⊢ (¬ 𝜑 → 𝜒) & ⊢ (¬ 𝜓 → 𝜒) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | ecase3d 1031 | Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (¬ (𝜓 ∨ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | ecased 1032 | Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜃)) & ⊢ (𝜑 → (¬ 𝜒 → 𝜃)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | ecase3ad 1033 | Deduction for elimination by cases. (Contributed by NM, 24-May-2013.) (Proof shortened by Wolf Lammen, 20-Sep-2024.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → ((¬ 𝜓 ∧ ¬ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | ecase3adOLD 1034 | Obsolete version of ecase3ad 1033 as of 20-Sep-2024. (Contributed by NM, 24-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → ((¬ 𝜓 ∧ ¬ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | ccase 1035 | Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜏) & ⊢ ((𝜒 ∧ 𝜓) → 𝜏) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) | ||
Theorem | ccased 1036 | Deduction for combining cases. (Contributed by NM, 9-May-2004.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂)) | ||
Theorem | ccase2 1037 | Inference for combining cases. (Contributed by NM, 29-Jul-1999.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜏) & ⊢ (𝜒 → 𝜏) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) | ||
Theorem | 4cases 1038 | Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) & ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | 4casesdan 1039 | Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) & ⊢ ((𝜑 ∧ (𝜓 ∧ ¬ 𝜒)) → 𝜃) & ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ 𝜒)) → 𝜃) & ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | cases 1040 | Case disjunction according to the value of 𝜑. (Contributed by NM, 25-Apr-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜓 ↔ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜃))) | ||
Theorem | dedlem0a 1041 | 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.) |
⊢ (𝜑 → (𝜓 ↔ ((𝜒 → 𝜑) → (𝜓 ∧ 𝜑)))) | ||
Theorem | dedlem0b 1042 | Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.) |
⊢ (¬ 𝜑 → (𝜓 ↔ ((𝜓 → 𝜑) → (𝜒 ∧ 𝜑)))) | ||
Theorem | dedlema 1043 | Lemma for weak deduction theorem. See also ifptru 1073. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) | ||
Theorem | dedlemb 1044 | Lemma for weak deduction theorem. See also ifpfal 1074. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) | ||
Theorem | cases2 1045 | Case disjunction according to the value of 𝜑. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 28-Feb-2022.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | cases2ALT 1046 | Alternate proof of cases2 1045, not using dedlema 1043 or dedlemb 1044. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 2-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | dfbi3 1047 | 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 | pm5.24 1048 | Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑))) | ||
Theorem | 4exmid 1049 | The disjunction of the four possible combinations of two wffs and their negations is always true. A four-way excluded middle (see exmid 892). (Contributed by David Abernethy, 28-Jan-2014.) (Proof shortened by NM, 29-Oct-2021.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ∨ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑))) | ||
Theorem | consensus 1050 | 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 | pm4.42 1051 | Theorem *4.42 of [WhiteheadRussell] p. 119. See also ifpid 1075. (Contributed by Roy F. Longton, 21-Jun-2005.) |
⊢ (𝜑 ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓))) | ||
Theorem | prlem1 1052 | A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
⊢ (𝜑 → (𝜂 ↔ 𝜒)) & ⊢ (𝜓 → ¬ 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (((𝜓 ∧ 𝜒) ∨ (𝜃 ∧ 𝜏)) → 𝜂))) | ||
Theorem | prlem2 1053 | A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 9-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∧ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)))) | ||
Theorem | oplem1 1054 | A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) & ⊢ (𝜑 → (𝜃 ∨ 𝜏)) & ⊢ (𝜓 ↔ 𝜃) & ⊢ (𝜒 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | dn1 1055 | A single axiom for Boolean algebra known as DN1. See McCune, Veroff, Fitelson, Harris, Feist, Wos, Short single axioms for Boolean algebra, Journal of Automated Reasoning, 29(1):1--16, 2002. (https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf). (Contributed by Jeff Hankins, 3-Jul-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 6-Jan-2013.) |
⊢ (¬ (¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) ↔ 𝜒) | ||
Theorem | bianir 1056 | A closed form of mpbir 230, analogous to pm2.27 42 (assertion). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Roger Witte, 17-Aug-2020.) |
⊢ ((𝜑 ∧ (𝜓 ↔ 𝜑)) → 𝜓) | ||
Theorem | jaoi2 1057 | Inference removing a negated conjunct in a disjunction of an antecedent if this conjunct is part of the disjunction. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) |
⊢ ((𝜑 ∨ (¬ 𝜑 ∧ 𝜒)) → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) → 𝜓) | ||
Theorem | jaoi3 1058 | Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018.) |
⊢ (𝜑 → 𝜓) & ⊢ ((¬ 𝜑 ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) → 𝜓) | ||
Theorem | ornld 1059 | 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.) |
⊢ (𝜑 → (((𝜑 → (𝜃 ∨ 𝜏)) ∧ ¬ 𝜃) → 𝜏)) | ||
This subsection introduces the conditional operator for propositions, denoted by if-(𝜑, 𝜓, 𝜒) (see df-ifp 1061). It is the analogue for propositions of the conditional operator for classes, denoted by if(𝜑, 𝐴, 𝐵) (see df-if 4466). | ||
Syntax | wif 1060 | Extend wff notation to include the conditional operator for propositions. |
wff if-(𝜑, 𝜓, 𝜒) | ||
Definition | df-ifp 1061 |
Definition of the conditional operator for propositions. The expression
if-(𝜑,
𝜓, 𝜒) is read "if 𝜑 then
𝜓
else 𝜒".
See dfifp2 1062, dfifp3 1063, dfifp4 1064, dfifp5 1065, dfifp6 1066 and dfifp7 1067 for
alternate definitions.
This definition (in the form of dfifp2 1062) appears in Section II.24 of [Church] p. 129 (Definition D12 page 132), where it is called "conditioned disjunction". Church's [𝜓, 𝜑, 𝜒] corresponds to our if-(𝜑, 𝜓, 𝜒) (note the permutation of the first two variables). This form was chosen as the definition rather than dfifp2 1062 for compatibility with intuitionistic logic development: with this form, it is clear that if-(𝜑, 𝜓, 𝜒) implies decidability of 𝜑, which is most often what is wanted. Church uses the conditional operator as an intermediate step to prove completeness of some systems of connectives. The first result is that the system {if-, ⊤, ⊥} is complete: for the induction step, consider a formula of n+1 variables; single out one variable, say 𝜑; when one sets 𝜑 to True (resp. False), then what remains is a formula of n variables, so by the induction hypothesis it is equivalent to a formula using only the connectives if-, ⊤, ⊥, say 𝜓 (resp. 𝜒); therefore, the formula if-(𝜑, 𝜓, 𝜒) is equivalent to the initial formula of n+1 variables. Now, since { → , ¬ } and similar systems suffice to express the connectives if-, ⊤, ⊥, they are also complete. (Contributed by BJ, 22-Jun-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) | ||
Theorem | dfifp2 1062 | Alternate definition of the conditional operator for propositions. The value of if-(𝜑, 𝜓, 𝜒) is "if 𝜑 then 𝜓, and if not 𝜑 then 𝜒". This is the definition used in Section II.24 of [Church] p. 129 (Definition D12 page 132) (see comment of df-ifp 1061). (Contributed by BJ, 22-Jun-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | dfifp3 1063 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (𝜑 ∨ 𝜒))) | ||
Theorem | dfifp4 1064 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒))) | ||
Theorem | dfifp5 1065 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | dfifp6 1066 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ ¬ (𝜒 → 𝜑))) | ||
Theorem | dfifp7 1067 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜒 → 𝜑) → (𝜑 ∧ 𝜓))) | ||
Theorem | ifpdfbi 1068 | Define the biconditional as conditional logic operator. (Contributed by RP, 20-Apr-2020.) (Proof shortened by Wolf Lammen, 30-Apr-2024.) |
⊢ ((𝜑 ↔ 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓)) | ||
Theorem | anifp 1069 | The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor 1070. (Contributed by BJ, 30-Sep-2019.) |
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpor 1070 | The conditional operator implies the disjunction of its possible outputs. Dual statement of anifp 1069. (Contributed by BJ, 1-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) → (𝜓 ∨ 𝜒)) | ||
Theorem | ifpn 1071 | Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019.) (Proof shortened by Wolf Lammen, 5-May-2024.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ if-(¬ 𝜑, 𝜒, 𝜓)) | ||
Theorem | ifpnOLD 1072 | Obsolete version of ifpn 1071 as of 5-May-2024. (Contributed by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ if-(¬ 𝜑, 𝜒, 𝜓)) | ||
Theorem | ifptru 1073 | Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue 4471. This is essentially dedlema 1043. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
⊢ (𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜓)) | ||
Theorem | ifpfal 1074 | Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of iffalse 4474. This is essentially dedlemb 1044. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.) |
⊢ (¬ 𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜒)) | ||
Theorem | ifpid 1075 | Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid 4505. This is essentially pm4.42 1051. (Contributed by BJ, 20-Sep-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓) | ||
Theorem | casesifp 1076 | Version of cases 1040 expressed using if-. Case disjunction according to the value of 𝜑. One can see this as a proof that the two hypotheses characterize the conditional operator for propositions. For the converses, see ifptru 1073 and ifpfal 1074. (Contributed by BJ, 20-Sep-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜓 ↔ if-(𝜑, 𝜒, 𝜃)) | ||
Theorem | ifpbi123d 1077 | Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 17-Apr-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜏)) & ⊢ (𝜑 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → (𝜃 ↔ 𝜁)) ⇒ ⊢ (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜏, 𝜂, 𝜁))) | ||
Theorem | ifpbi123dOLD 1078 | Obsolete version of ifpbi123d 1077 as of 17-Apr-2024. (Contributed by AV, 30-Dec-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜏)) & ⊢ (𝜑 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → (𝜃 ↔ 𝜁)) ⇒ ⊢ (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜏, 𝜂, 𝜁))) | ||
Theorem | ifpbi23d 1079 | Equivalence deduction for conditional operator for propositions. Convenience theorem for a frequent case. (Contributed by Wolf Lammen, 28-Apr-2024.) |
⊢ (𝜑 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → (𝜃 ↔ 𝜁)) ⇒ ⊢ (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜓, 𝜂, 𝜁))) | ||
Theorem | ifpimpda 1080 | Separation of the values of the conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 27-Feb-2021.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜃) ⇒ ⊢ (𝜑 → if-(𝜓, 𝜒, 𝜃)) | ||
Theorem | 1fpid3 1081 | The value of the conditional operator for propositions is its third argument if the first and second argument imply the third argument. (Contributed by AV, 4-Apr-2021.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (if-(𝜑, 𝜓, 𝜒) → 𝜒) | ||
This subsection contains a few results related to the weak deduction theorem in propositional calculus. For the weak deduction theorem in set theory, see the section beginning with dedth 4523. For more information on the weak deduction theorem, see the Weak Deduction Theorem page mmdeduction.html 4523. | ||
Theorem | elimh 1082 | Hypothesis builder for the weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html. (Contributed by NM, 26-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) Commute consequent. (Revised by Steven Nguyen, 27-Apr-2023.) |
⊢ ((if-(𝜒, 𝜑, 𝜓) ↔ 𝜑) → (𝜏 ↔ 𝜒)) & ⊢ ((if-(𝜒, 𝜑, 𝜓) ↔ 𝜓) → (𝜏 ↔ 𝜃)) & ⊢ 𝜃 ⇒ ⊢ 𝜏 | ||
Theorem | dedt 1083 | The weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html. (Contributed by NM, 26-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) Commute consequent. (Revised by Steven Nguyen, 27-Apr-2023.) |
⊢ ((if-(𝜒, 𝜑, 𝜓) ↔ 𝜑) → (𝜏 ↔ 𝜃)) & ⊢ 𝜏 ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | con3ALT 1084 | Proof of con3 153 from its associated inference con3i 154 that illustrates the use of the weak deduction theorem dedt 1083. (Contributed by NM, 27-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) Revised dedt 1083 and elimh 1082. (Revised by Steven Nguyen, 27-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||
Syntax | w3o 1085 | Extend wff definition to include three-way disjunction ('or'). |
wff (𝜑 ∨ 𝜓 ∨ 𝜒) | ||
Syntax | w3a 1086 | Extend wff definition to include three-way conjunction ('and'). |
wff (𝜑 ∧ 𝜓 ∧ 𝜒) | ||
Definition | df-3or 1087 | Define disjunction ('or') of three wff's. Definition *2.33 of [WhiteheadRussell] p. 105. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law orass 919. (Contributed by NM, 8-Apr-1994.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) | ||
Definition | df-3an 1088 | Define conjunction ('and') of three wff's. Definition *4.34 of [WhiteheadRussell] p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass 469. (Contributed by NM, 8-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | ||
Theorem | 3orass 1089 | Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | 3orel1 1090 | Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.) |
⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜓 ∨ 𝜒))) | ||
Theorem | 3orrot 1091 | Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) | ||
Theorem | 3orcoma 1092 | Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜑 ∨ 𝜒)) | ||
Theorem | 3orcomb 1093 | Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.) (Proof shortened by Wolf Lammen, 8-Apr-2022.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓)) | ||
Theorem | 3anass 1094 | Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | ||
Theorem | 3anan12 1095 | Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised to shorten 3ancoma 1097 by Wolf Lammen, 5-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | ||
Theorem | 3anan32 1096 | Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | ||
Theorem | 3ancoma 1097 | Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 5-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) | ||
Theorem | 3ancomb 1098 | Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Revised to shorten 3anrot 1099 by Wolf Lammen, 9-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) | ||
Theorem | 3anrot 1099 | Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 9-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) | ||
Theorem | 3anrev 1100 | Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓 ∧ 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |