Home | Metamath
Proof Explorer Theorem List (p. 3 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 | mt2 201 | A rule similar to modus tollens. Inference associated with con2i 141. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.) |
⊢ 𝜓 & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | mt3 202 | A rule similar to modus tollens. Inference associated with con1i 149. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ ¬ 𝜓 & ⊢ (¬ 𝜑 → 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | peirce 203 | Peirce's axiom. A non-intuitionistic implication-only statement. Added to intuitionistic (implicational) propositional calculus, it gives classical (implicational) propositional calculus. For another non-intuitionistic positive statement, see curryax 887. When ⊥ is substituted for 𝜓, then this becomes the Clavius law pm2.18 128. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 9-Oct-2012.) |
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑) | ||
Theorem | looinv 204 | The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 895, we can see that this essentially expresses "disjunction commutes". Theorem *2.69 of [WhiteheadRussell] p. 108. It is a special instance of the axiom "Roll", see peirceroll 85. (Contributed by NM, 12-Aug-2004.) |
⊢ (((𝜑 → 𝜓) → 𝜓) → ((𝜓 → 𝜑) → 𝜑)) | ||
Theorem | bijust0 205 | A self-implication (see id 22) does not imply its own negation. The justification theorem bijust 206 is one of its instances. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) Extract bijust0 205 from proof of bijust 206. (Revised by BJ, 19-Mar-2020.) |
⊢ ¬ ((𝜑 → 𝜑) → ¬ (𝜑 → 𝜑)) | ||
Theorem | bijust 206 | Theorem used to justify the definition of the biconditional df-bi 208. Instance of bijust0 205. (Contributed by NM, 11-May-1999.) |
⊢ ¬ ((¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))) | ||
The definition df-bi 208 in this section is our first definition, which introduces and defines the biconditional connective ↔ used to denote logical equivalence. We define a wff of the form (𝜑 ↔ 𝜓) as an abbreviation for ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)). Unlike most traditional developments, we have chosen not to have a separate symbol such as "Df." to mean "is defined as". Instead, we will later use the biconditional connective for this purpose (df-an 397 is its first use), as it allows us to use logic to manipulate definitions directly. This greatly simplifies many proofs since it eliminates the need for a separate mechanism for introducing and eliminating definitions. A note on definitions: definitions are required to be eliminable (that is, a theorem stated in terms of the defined symbol can also be stated without it) and conservative (that is, a theorem whose statement does not contain the defined symbol can be proved without using that definition). This means that a definition does not increase the expressive power nor the deductive power, respectively, of a theory. On the other hand, definitions are often useful to write shorter proofs, so in (i)set.mm we will generally not try to avoid them. This is why, for instance, some theorems which do not contain disjunction in their statement are placed after the section on disjunction because a shorter proof using disjunction is possible. | ||
Syntax | wb 207 | Extend wff definition to include the biconditional connective. |
wff (𝜑 ↔ 𝜓) | ||
Definition | df-bi 208 |
Define the biconditional (logical "iff" or "if and only
if").
The definition df-bi 208 in this section is our first definition, which introduces and defines the biconditional connective ↔. We define a wff of the form (𝜑 ↔ 𝜓) as an abbreviation for ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)). Unlike most traditional developments, we have chosen not to have a separate symbol such as "Df." to mean "is defined as". Instead, we will later use the biconditional connective for this purpose (df-or 842 is its first use), as it allows us to use logic to manipulate definitions directly. This greatly simplifies many proofs since it eliminates the need for a separate mechanism for introducing and eliminating definitions. Of course, we cannot use this mechanism to define the biconditional itself, since it hasn't been introduced yet. Instead, we use a more general form of definition, described as follows. In its most general form, a definition is simply an assertion that introduces a new symbol (or a new combination of existing symbols, as in df-3an 1081) that is eliminable and does not strengthen the existing language. The latter requirement means that the set of provable statements not containing the new symbol (or new combination) should remain exactly the same after the definition is introduced. Our definition of the biconditional may look unusual compared to most definitions, but it strictly satisfies these requirements. The justification for our definition is that if we mechanically replace (𝜑 ↔ 𝜓) (the definiendum i.e. the thing being defined) with ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) (the definiens i.e. the defining expression) in the definition, the definition becomes the previously proved theorem bijust 206. It is impossible to use df-bi 208 to prove any statement expressed in the original language that can't be proved from the original axioms, because if we simply replace each instance of df-bi 208 in the proof with the corresponding bijust 206 instance, we will end up with a proof from the original axioms. Note that from Metamath's point of view, a definition is just another axiom - i.e. an assertion we claim to be true - but from our high level point of view, we are not strengthening the language. To indicate this fact, we prefix definition labels with "df-" instead of "ax-". (This prefixing is an informal convention that means nothing to the Metamath proof verifier; it is just a naming convention for human readability.) After we define the constant true ⊤ (df-tru 1531) and the constant false ⊥ (df-fal 1541), we will be able to prove these truth table values: ((⊤ ↔ ⊤) ↔ ⊤) (trubitru 1557), ((⊤ ↔ ⊥) ↔ ⊥) (trubifal 1559), ((⊥ ↔ ⊤) ↔ ⊥) (falbitru 1558), and ((⊥ ↔ ⊥) ↔ ⊤) (falbifal 1560). See dfbi1 214, dfbi2 475, and dfbi3 1041 for theorems suggesting typical textbook definitions of ↔, showing that our definition has the properties we expect. Theorem dfbi1 214 is particularly useful if we want to eliminate ↔ from an expression to convert it to primitives. Theorem dfbi 476 shows this definition rewritten in an abbreviated form after conjunction is introduced, for easier understanding. Contrast with ∨ (df-or 842), → (wi 4), ⊼ (df-nan 1476), and ⊻ (df-xor 1496). In some sense ↔ returns true if two truth values are equal; = (df-cleq 2814) returns true if two classes are equal. (Contributed by NM, 27-Dec-1992.) |
⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | ||
Theorem | impbi 209 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓))) | ||
Theorem | impbii 210 | Infer an equivalence from an implication and its converse. Inference associated with impbi 209. (Contributed by NM, 29-Dec-1992.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜑) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | impbidd 211 | Deduce an equivalence from two implications. Double deduction associated with impbi 209 and impbii 210. Deduction associated with impbid 213. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | ||
Theorem | impbid21d 212 | Deduce an equivalence from two implications. (Contributed by Wolf Lammen, 12-May-2013.) |
⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (𝜃 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | ||
Theorem | impbid 213 | Deduce an equivalence from two implications. Deduction associated with impbi 209 and impbii 210. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 212. (Revised by Wolf Lammen, 3-Nov-2012.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | dfbi1 214 | Relate the biconditional connective to primitive connectives. See dfbi1ALT 215 for an unusual version proved directly from axioms. (Contributed by NM, 29-Dec-1992.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | ||
Theorem | dfbi1ALT 215 | Alternate proof of dfbi1 214. This proof, discovered by Gregory Bush on 8-Mar-2004, has several curious properties. First, it has only 17 steps directly from the axioms and df-bi 208, compared to over 800 steps were the proof of dfbi1 214 expanded into axioms. Second, step 2 demands only the property of "true"; any axiom (or theorem) could be used. It might be thought, therefore, that it is in some sense redundant, but in fact no proof is shorter than this (measured by number of steps). Third, it illustrates how intermediate steps can "blow up" in size even in short proofs. Fourth, the compressed proof is only 182 bytes (or 17 bytes in D-proof notation), but the generated web page is over 200kB with intermediate steps that are essentially incomprehensible to humans (other than Gregory Bush). If there were an obfuscated code contest for proofs, this would be a contender. This "blowing up" and incomprehensibility of the intermediate steps vividly demonstrate the advantages of using many layered intermediate theorems, since each theorem is easier to understand. (Contributed by Gregory Bush, 10-Mar-2004.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | ||
Theorem | biimp 216 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | biimpi 217 | Infer an implication from a logical equivalence. Inference associated with biimp 216. (Contributed by NM, 29-Dec-1992.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | sylbi 218 | A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | sylib 219 | A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | sylbb 220 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | biimpr 221 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | bicom1 222 | Commutative law for the biconditional. (Contributed by Wolf Lammen, 10-Nov-2012.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
Theorem | bicom 223 | Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) |
⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑)) | ||
Theorem | bicomd 224 | Commute two sides of a biconditional in a deduction. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ↔ 𝜓)) | ||
Theorem | bicomi 225 | Inference from commutative law for logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜓 ↔ 𝜑) | ||
Theorem | impbid1 226 | Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | impbid2 227 | Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.) |
⊢ (𝜓 → 𝜒) & ⊢ (𝜑 → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | impcon4bid 228 | A variation on impbid 213 with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | biimpri 229 | Infer a converse implication from a logical equivalence. Inference associated with biimpr 221. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 16-Sep-2013.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜓 → 𝜑) | ||
Theorem | biimpd 230 | Deduce an implication from a logical equivalence. Deduction associated with biimp 216 and biimpi 217. (Contributed by NM, 11-Jan-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | mpbi 231 | An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-1993.) |
⊢ 𝜑 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | mpbir 232 | An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.) |
⊢ 𝜓 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | mpbid 233 | A deduction from a biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | mpbii 234 | An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
⊢ 𝜓 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | sylibr 235 | A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | sylbir 236 | A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | sylbbr 237 |
A mixed syllogism inference from two biconditionals.
Note on the various syllogism-like statements in set.mm. The hypothetical syllogism syl 17 infers an implication from two implications (and there are 3syl 18 and 4syl 19 for chaining more inferences). There are four inferences inferring an implication from one implication and one biconditional: sylbi 218, sylib 219, sylbir 236, sylibr 235; four inferences inferring an implication from two biconditionals: sylbb 220, sylbbr 237, sylbb1 238, sylbb2 239; four inferences inferring a biconditional from two biconditionals: bitri 276, bitr2i 277, bitr3i 278, bitr4i 279 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 47, syl5 34, syl6 35, mpbid 233, bitrd 280, syl5bb 284, syl6bb 288 and variants. (Contributed by BJ, 21-Apr-2019.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜒 → 𝜑) | ||
Theorem | sylbb1 238 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜑 ↔ 𝜒) ⇒ ⊢ (𝜓 → 𝜒) | ||
Theorem | sylbb2 239 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | sylibd 240 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | sylbid 241 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | mpbidi 242 | A deduction from a biconditional, related to modus ponens. (Contributed by NM, 9-Aug-1994.) |
⊢ (𝜃 → (𝜑 → 𝜓)) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜃 → (𝜑 → 𝜒)) | ||
Theorem | syl5bi 243 | A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 12-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → (𝜓 → 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 → 𝜃)) | ||
Theorem | syl5bir 244 | A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜒 → (𝜓 → 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 → 𝜃)) | ||
Theorem | syl5ib 245 | A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 → 𝜃)) | ||
Theorem | syl5ibcom 246 | A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜒 → 𝜃)) | ||
Theorem | syl5ibr 247 | A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝜑 → 𝜃) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 → 𝜓)) | ||
Theorem | syl5ibrcom 248 | A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.) |
⊢ (𝜑 → 𝜃) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | biimprd 249 | Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 221 and biimpri 229. (Contributed by NM, 11-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | biimpcd 250 | Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜓 → (𝜑 → 𝜒)) | ||
Theorem | biimprcd 251 | Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜒 → (𝜑 → 𝜓)) | ||
Theorem | syl6ib 252 | A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | syl6ibr 253 | A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | syl6bi 254 | A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | syl6bir 255 | A mixed syllogism inference. (Contributed by NM, 18-May-1994.) |
⊢ (𝜑 → (𝜒 ↔ 𝜓)) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | syl7bi 256 | A mixed syllogism inference from a doubly nested implication and a biconditional. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏))) ⇒ ⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏))) | ||
Theorem | syl8ib 257 | A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜃 ↔ 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) | ||
Theorem | mpbird 258 | A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | mpbiri 259 | An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
⊢ 𝜒 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | sylibrd 260 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | sylbird 261 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝜑 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | biid 262 | Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. This is part of Frege's eighth axiom per Proposition 54 of [Frege1879] p. 50; see also eqid 2821. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜑 ↔ 𝜑) | ||
Theorem | biidd 263 | Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜓)) | ||
Theorem | pm5.1im 264 | Two propositions are equivalent if they are both true. Closed form of 2th 265. Equivalent to a biimp 216-like version of the xor-connective. This theorem stays true, no matter how you permute its operands. This is evident from its sharper version (𝜑 ↔ (𝜓 ↔ (𝜑 ↔ 𝜓))). (Contributed by Wolf Lammen, 12-May-2013.) |
⊢ (𝜑 → (𝜓 → (𝜑 ↔ 𝜓))) | ||
Theorem | 2th 265 | Two truths are equivalent. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | 2thd 266 | Two truths are equivalent. Deduction form. (Contributed by NM, 3-Jun-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | monothetic 267 | Two self-implications (see id 22) are equivalent. This theorem, rather trivial in our axiomatization, is (the biconditional form of) a standard axiom for monothetic BCI logic. This is the most general theorem of which trujust 1530 is an instance. Relatedly, this would be the justification theorem if the definition of ⊤ were dftru2 1533. (Contributed by BJ, 7-Sep-2022.) |
⊢ ((𝜑 → 𝜑) ↔ (𝜓 → 𝜓)) | ||
Theorem | ibi 268 | Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.) |
⊢ (𝜑 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | ibir 269 | Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.) |
⊢ (𝜑 → (𝜓 ↔ 𝜑)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | ibd 270 | Deduction that converts a biconditional implied by one of its arguments, into an implication. Deduction associated with ibi 268. (Contributed by NM, 26-Jun-2004.) |
⊢ (𝜑 → (𝜓 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | pm5.74 271 | Distribution of implication over biconditional. Theorem *5.74 of [WhiteheadRussell] p. 126. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 11-Apr-2013.) |
⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))) | ||
Theorem | pm5.74i 272 | Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) | ||
Theorem | pm5.74ri 273 | Distribution of implication over biconditional (reverse inference form). (Contributed by NM, 1-Aug-1994.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | pm5.74d 274 | Distribution of implication over biconditional (deduction form). (Contributed by NM, 21-Mar-1996.) |
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) | ||
Theorem | pm5.74rd 275 | Distribution of implication over biconditional (deduction form). (Contributed by NM, 19-Mar-1997.) |
⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | ||
Theorem | bitri 276 | An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | bitr2i 277 | An inference from transitive law for logical equivalence. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜒 ↔ 𝜑) | ||
Theorem | bitr3i 278 | An inference from transitive law for logical equivalence. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | bitr4i 279 | An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | bitrd 280 | Deduction form of bitri 276. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | bitr2d 281 | Deduction form of bitr2i 277. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | ||
Theorem | bitr3d 282 | Deduction form of bitr3i 278. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜒 ↔ 𝜃)) | ||
Theorem | bitr4d 283 | Deduction form of bitr4i 279. (Contributed by NM, 30-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | syl5bb 284 | A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 ↔ 𝜃)) | ||
Theorem | syl5rbb 285 | A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜃 ↔ 𝜑)) | ||
Theorem | syl5bbr 286 | A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 ↔ 𝜃)) | ||
Theorem | syl5rbbr 287 | A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜃 ↔ 𝜑)) | ||
Theorem | syl6bb 288 | A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | syl6rbb 289 | A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | ||
Theorem | syl6bbr 290 | A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | syl6rbbr 291 | A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | ||
Theorem | 3imtr3i 292 | A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 ↔ 𝜒) & ⊢ (𝜓 ↔ 𝜃) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | 3imtr4i 293 | A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | 3imtr3d 294 | More general version of 3imtr3i 292. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → (𝜒 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜃 → 𝜏)) | ||
Theorem | 3imtr4d 295 | More general version of 3imtr4i 293. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜓)) & ⊢ (𝜑 → (𝜏 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜃 → 𝜏)) | ||
Theorem | 3imtr3g 296 | More general version of 3imtr3i 292. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜓 ↔ 𝜃) & ⊢ (𝜒 ↔ 𝜏) ⇒ ⊢ (𝜑 → (𝜃 → 𝜏)) | ||
Theorem | 3imtr4g 297 | More general version of 3imtr4i 293. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 → 𝜏)) | ||
Theorem | 3bitri 298 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 ↔ 𝜃) | ||
Theorem | 3bitrri 299 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜃 ↔ 𝜑) | ||
Theorem | 3bitr2i 300 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 ↔ 𝜃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |