![]() |
Metamath
Proof Explorer Theorem List (p. 11 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oranabs 1001 | 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 1002 | Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.) |
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ 𝜓) ↔ (𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm5.6 1003 | Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.) |
⊢ (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒))) | ||
Theorem | orcanai 1004 | Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) | ||
Theorem | pm4.79 1005 | Theorem *4.79 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2013.) |
⊢ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜑)) ↔ ((𝜓 ∧ 𝜒) → 𝜑)) | ||
Theorem | pm5.53 1006 | Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((((𝜑 ∨ 𝜓) ∨ 𝜒) → 𝜃) ↔ (((𝜑 → 𝜃) ∧ (𝜓 → 𝜃)) ∧ (𝜒 → 𝜃))) | ||
Theorem | ordi 1007 | 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 1008 | Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))) | ||
Theorem | andi 1009 | 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 1010 | Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
Theorem | orddi 1011 | Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)) ↔ (((𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜃)) ∧ ((𝜓 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)))) | ||
Theorem | anddi 1012 | Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)) ∨ ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))) | ||
Theorem | pm5.17 1013 | Theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | pm5.15 1014 | Theorem *5.15 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 15-Oct-2013.) |
⊢ ((𝜑 ↔ 𝜓) ∨ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | pm5.16 1015 | Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 17-Oct-2013.) |
⊢ ¬ ((𝜑 ↔ 𝜓) ∧ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | xor 1016 | Two ways to express exclusive disjunction (df-xor 1508). Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.) |
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑))) | ||
Theorem | nbi2 1017 | Two ways to express "exclusive or". (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.) |
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) | ||
Theorem | xordi 1018 | 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 1522 does hold in it. (Contributed by NM, 3-Oct-2008.) |
⊢ ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) | ||
Theorem | pm5.54 1019 | Theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 7-Nov-2013.) |
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∧ 𝜓) ↔ 𝜓)) | ||
Theorem | pm5.62 1020 | Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm5.63 1021 | Theorem *5.63 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 25-Dec-2012.) |
⊢ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓))) | ||
Theorem | niabn 1022 | Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑)) | ||
Theorem | ninba 1023 | Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓))) | ||
Theorem | pm4.43 1024 | Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.) |
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓))) | ||
Theorem | pm4.82 1025 | Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑) | ||
Theorem | pm4.83 1026 | Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓) | ||
Theorem | pclem6 1027 | Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.) |
⊢ ((𝜑 ↔ (𝜓 ∧ ¬ 𝜑)) → ¬ 𝜓) | ||
Theorem | bigolden 1028 | Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.) |
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | pm5.71 1029 | Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.) |
⊢ ((𝜓 → ¬ 𝜒) → (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ 𝜒))) | ||
Theorem | pm5.75 1030 | 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 1031 | Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Sep-2024.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) & ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜃)) & ⊢ (𝜑 → (𝜏 ∨ (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | ecase3 1032 | Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜓 → 𝜒) & ⊢ (¬ (𝜑 ∨ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | ecase 1033 | Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.) |
⊢ (¬ 𝜑 → 𝜒) & ⊢ (¬ 𝜓 → 𝜒) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | ecase3d 1034 | Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (¬ (𝜓 ∨ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | ecased 1035 | Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜃)) & ⊢ (𝜑 → (¬ 𝜒 → 𝜃)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | ecase3ad 1036 | Deduction for elimination by cases. (Contributed by NM, 24-May-2013.) (Proof shortened by Wolf Lammen, 20-Sep-2024.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → ((¬ 𝜓 ∧ ¬ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | ccase 1037 | Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜏) & ⊢ ((𝜒 ∧ 𝜓) → 𝜏) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) | ||
Theorem | ccased 1038 | Deduction for combining cases. (Contributed by NM, 9-May-2004.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂)) | ||
Theorem | ccase2 1039 | Inference for combining cases. (Contributed by NM, 29-Jul-1999.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜏) & ⊢ (𝜒 → 𝜏) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) | ||
Theorem | 4cases 1040 | Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) & ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | 4casesdan 1041 | Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) & ⊢ ((𝜑 ∧ (𝜓 ∧ ¬ 𝜒)) → 𝜃) & ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ 𝜒)) → 𝜃) & ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | cases 1042 | Case disjunction according to the value of 𝜑. (Contributed by NM, 25-Apr-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜓 ↔ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜃))) | ||
Theorem | dedlem0a 1043 | 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 1044 | Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.) |
⊢ (¬ 𝜑 → (𝜓 ↔ ((𝜓 → 𝜑) → (𝜒 ∧ 𝜑)))) | ||
Theorem | dedlema 1045 | Lemma for weak deduction theorem. See also ifptru 1074. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) | ||
Theorem | dedlemb 1046 | Lemma for weak deduction theorem. See also ifpfal 1075. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) | ||
Theorem | cases2 1047 | Case disjunction according to the value of 𝜑. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 28-Feb-2022.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | cases2ALT 1048 | Alternate proof of cases2 1047, not using dedlema 1045 or dedlemb 1046. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 2-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | dfbi3 1049 | 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 1050 | Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑))) | ||
Theorem | 4exmid 1051 | The disjunction of the four possible combinations of two wffs and their negations is always true. A four-way excluded middle (see exmid 894). (Contributed by David Abernethy, 28-Jan-2014.) (Proof shortened by NM, 29-Oct-2021.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ∨ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑))) | ||
Theorem | consensus 1052 | 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 1053 | Theorem *4.42 of [WhiteheadRussell] p. 119. See also ifpid 1076. (Contributed by Roy F. Longton, 21-Jun-2005.) |
⊢ (𝜑 ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓))) | ||
Theorem | prlem1 1054 | 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 1055 | 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 1056 | 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 1057 | 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 1058 | A closed form of mpbir 231, analogous to pm2.27 42 (assertion). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Roger Witte, 17-Aug-2020.) |
⊢ ((𝜑 ∧ (𝜓 ↔ 𝜑)) → 𝜓) | ||
Theorem | jaoi2 1059 | 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 1060 | Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018.) |
⊢ (𝜑 → 𝜓) & ⊢ ((¬ 𝜑 ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) → 𝜓) | ||
Theorem | ornld 1061 | 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 1063). It is the analogue for propositions of the conditional operator for classes, denoted by if(𝜑, 𝐴, 𝐵) (see df-if 4531). | ||
Syntax | wif 1062 | Extend wff notation to include the conditional operator for propositions. |
wff if-(𝜑, 𝜓, 𝜒) | ||
Definition | df-ifp 1063 |
Definition of the conditional operator for propositions. The expression
if-(𝜑,
𝜓, 𝜒) is read "if 𝜑 then
𝜓
else 𝜒".
See dfifp2 1064, dfifp3 1065, dfifp4 1066, dfifp5 1067, dfifp6 1068 and dfifp7 1069 for
alternate definitions.
This definition (in the form of dfifp2 1064) 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 1064 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 1064 | 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 1063). (Contributed by BJ, 22-Jun-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | dfifp3 1065 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (𝜑 ∨ 𝜒))) | ||
Theorem | dfifp4 1066 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒))) | ||
Theorem | dfifp5 1067 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | dfifp6 1068 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ ¬ (𝜒 → 𝜑))) | ||
Theorem | dfifp7 1069 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜒 → 𝜑) → (𝜑 ∧ 𝜓))) | ||
Theorem | ifpdfbi 1070 | Define the biconditional as conditional logic operator. (Contributed by RP, 20-Apr-2020.) (Proof shortened by Wolf Lammen, 30-Apr-2024.) |
⊢ ((𝜑 ↔ 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓)) | ||
Theorem | anifp 1071 | The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor 1072. (Contributed by BJ, 30-Sep-2019.) |
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpor 1072 | The conditional operator implies the disjunction of its possible outputs. Dual statement of anifp 1071. (Contributed by BJ, 1-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) → (𝜓 ∨ 𝜒)) | ||
Theorem | ifpn 1073 | 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 | ifptru 1074 | Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue 4536. This is essentially dedlema 1045. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
⊢ (𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜓)) | ||
Theorem | ifpfal 1075 | Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of iffalse 4539. This is essentially dedlemb 1046. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.) |
⊢ (¬ 𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜒)) | ||
Theorem | ifpid 1076 | Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid 4570. This is essentially pm4.42 1053. (Contributed by BJ, 20-Sep-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓) | ||
Theorem | casesifp 1077 | Version of cases 1042 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 1074 and ifpfal 1075. (Contributed by BJ, 20-Sep-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜓 ↔ if-(𝜑, 𝜒, 𝜃)) | ||
Theorem | ifpbi123d 1078 | Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 17-Apr-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜏)) & ⊢ (𝜑 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → (𝜃 ↔ 𝜁)) ⇒ ⊢ (𝜑 → (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 4588. For more information on the weak deduction theorem, see the Weak Deduction Theorem page mmdeduction.html 4588. | ||
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 921. (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 468. (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 > |