![]() |
Metamath
Proof Explorer Theorem List (p. 3 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | impbii 201 | Infer an equivalence from an implication and its converse. Inference associated with impbi 200. (Contributed by NM, 29-Dec-1992.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜑) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | impbidd 202 | Deduce an equivalence from two implications. Double deduction associated with impbi 200 and impbii 201. Deduction associated with impbid 204. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | ||
Theorem | impbid21d 203 | Deduce an equivalence from two implications. (Contributed by Wolf Lammen, 12-May-2013.) |
⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (𝜃 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | ||
Theorem | impbid 204 | Deduce an equivalence from two implications. Deduction associated with impbi 200 and impbii 201. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 203. (Revised by Wolf Lammen, 3-Nov-2012.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | dfbi1 205 | Relate the biconditional connective to primitive connectives. See dfbi1ALT 206 for an unusual version proved directly from axioms. (Contributed by NM, 29-Dec-1992.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | ||
Theorem | dfbi1ALT 206 | Alternate proof of dfbi1 205. 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 199, compared to over 800 steps were the proof of dfbi1 205 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 207 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | biimpi 208 | Infer an implication from a logical equivalence. Inference associated with biimp 207. (Contributed by NM, 29-Dec-1992.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | sylbi 209 | 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 210 | A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | sylbb 211 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | biimpr 212 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | bicom1 213 | Commutative law for the biconditional. (Contributed by Wolf Lammen, 10-Nov-2012.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
Theorem | bicom 214 | Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) |
⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑)) | ||
Theorem | bicomd 215 | Commute two sides of a biconditional in a deduction. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ↔ 𝜓)) | ||
Theorem | bicomi 216 | Inference from commutative law for logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜓 ↔ 𝜑) | ||
Theorem | impbid1 217 | Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | impbid2 218 | Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.) |
⊢ (𝜓 → 𝜒) & ⊢ (𝜑 → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | impcon4bid 219 | A variation on impbid 204 with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | biimpri 220 | Infer a converse implication from a logical equivalence. Inference associated with biimpr 212. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 16-Sep-2013.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜓 → 𝜑) | ||
Theorem | biimpd 221 | Deduce an implication from a logical equivalence. Deduction associated with biimp 207 and biimpi 208. (Contributed by NM, 11-Jan-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | mpbi 222 | An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-1993.) |
⊢ 𝜑 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | mpbir 223 | An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.) |
⊢ 𝜓 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | mpbid 224 | A deduction from a biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | mpbii 225 | 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 226 | 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 227 | A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | sylbbr 228 |
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 209, sylib 210, sylbir 227, sylibr 226; four inferences inferring an implication from two biconditionals: sylbb 211, sylbbr 228, sylbb1 229, sylbb2 230; four inferences inferring a biconditional from two biconditionals: bitri 267, bitr2i 268, bitr3i 269, bitr4i 270 (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 224, bitrd 271, syl5bb 275, syl6bb 279 and variants. (Contributed by BJ, 21-Apr-2019.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜒 → 𝜑) | ||
Theorem | sylbb1 229 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜑 ↔ 𝜒) ⇒ ⊢ (𝜓 → 𝜒) | ||
Theorem | sylbb2 230 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | sylibd 231 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | sylbid 232 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | mpbidi 233 | A deduction from a biconditional, related to modus ponens. (Contributed by NM, 9-Aug-1994.) |
⊢ (𝜃 → (𝜑 → 𝜓)) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜃 → (𝜑 → 𝜒)) | ||
Theorem | syl5bi 234 | 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 235 | A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜒 → (𝜓 → 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 → 𝜃)) | ||
Theorem | syl5ib 236 | A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 → 𝜃)) | ||
Theorem | syl5ibcom 237 | A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜒 → 𝜃)) | ||
Theorem | syl5ibr 238 | A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝜑 → 𝜃) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 → 𝜓)) | ||
Theorem | syl5ibrcom 239 | A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.) |
⊢ (𝜑 → 𝜃) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | biimprd 240 | Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 212 and biimpri 220. (Contributed by NM, 11-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | biimpcd 241 | Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜓 → (𝜑 → 𝜒)) | ||
Theorem | biimprcd 242 | 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 243 | A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | syl6ibr 244 | 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 245 | A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | syl6bir 246 | A mixed syllogism inference. (Contributed by NM, 18-May-1994.) |
⊢ (𝜑 → (𝜒 ↔ 𝜓)) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | syl7bi 247 | A mixed syllogism inference from a doubly nested implication and a biconditional. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏))) ⇒ ⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏))) | ||
Theorem | syl8ib 248 | 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 249 | A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | mpbiri 250 | 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 251 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | sylbird 252 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝜑 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | biid 253 | 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 2778. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜑 ↔ 𝜑) | ||
Theorem | biidd 254 | Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜓)) | ||
Theorem | pm5.1im 255 | Two propositions are equivalent if they are both true. Closed form of 2th 256. Equivalent to a biimp 207-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 256 | Two truths are equivalent. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | 2thd 257 | Two truths are equivalent. Deduction form. (Contributed by NM, 3-Jun-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | monothetic 258 | 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 1603 is an instance. Relatedly, this would be the justification theorem if the definition of ⊤ were dftru2 1607. (Contributed by BJ, 7-Sep-2022.) |
⊢ ((𝜑 → 𝜑) ↔ (𝜓 → 𝜓)) | ||
Theorem | ibi 259 | Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.) |
⊢ (𝜑 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | ibir 260 | Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.) |
⊢ (𝜑 → (𝜓 ↔ 𝜑)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | ibd 261 | Deduction that converts a biconditional implied by one of its arguments, into an implication. Deduction associated with ibi 259. (Contributed by NM, 26-Jun-2004.) |
⊢ (𝜑 → (𝜓 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | pm5.74 262 | 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 263 | Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) | ||
Theorem | pm5.74ri 264 | Distribution of implication over biconditional (reverse inference form). (Contributed by NM, 1-Aug-1994.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | pm5.74d 265 | Distribution of implication over biconditional (deduction form). (Contributed by NM, 21-Mar-1996.) |
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) | ||
Theorem | pm5.74rd 266 | Distribution of implication over biconditional (deduction form). (Contributed by NM, 19-Mar-1997.) |
⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | ||
Theorem | bitri 267 | An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | bitr2i 268 | An inference from transitive law for logical equivalence. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜒 ↔ 𝜑) | ||
Theorem | bitr3i 269 | An inference from transitive law for logical equivalence. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | bitr4i 270 | An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | bitrd 271 | Deduction form of bitri 267. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | bitr2d 272 | Deduction form of bitr2i 268. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | ||
Theorem | bitr3d 273 | Deduction form of bitr3i 269. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜒 ↔ 𝜃)) | ||
Theorem | bitr4d 274 | Deduction form of bitr4i 270. (Contributed by NM, 30-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | syl5bb 275 | A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 ↔ 𝜃)) | ||
Theorem | syl5rbb 276 | A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜃 ↔ 𝜑)) | ||
Theorem | syl5bbr 277 | A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜑 ↔ 𝜃)) | ||
Theorem | syl5rbbr 278 | A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜒 → (𝜃 ↔ 𝜑)) | ||
Theorem | syl6bb 279 | A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | syl6rbb 280 | A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | ||
Theorem | syl6bbr 281 | A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | syl6rbbr 282 | A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | ||
Theorem | 3imtr3i 283 | A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 ↔ 𝜒) & ⊢ (𝜓 ↔ 𝜃) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | 3imtr4i 284 | A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | 3imtr3d 285 | More general version of 3imtr3i 283. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → (𝜒 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜃 → 𝜏)) | ||
Theorem | 3imtr4d 286 | More general version of 3imtr4i 284. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜓)) & ⊢ (𝜑 → (𝜏 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜃 → 𝜏)) | ||
Theorem | 3imtr3g 287 | More general version of 3imtr3i 283. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜓 ↔ 𝜃) & ⊢ (𝜒 ↔ 𝜏) ⇒ ⊢ (𝜑 → (𝜃 → 𝜏)) | ||
Theorem | 3imtr4g 288 | More general version of 3imtr4i 284. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 → 𝜏)) | ||
Theorem | 3bitri 289 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 ↔ 𝜃) | ||
Theorem | 3bitrri 290 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ 𝜒) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜃 ↔ 𝜑) | ||
Theorem | 3bitr2i 291 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 ↔ 𝜃) | ||
Theorem | 3bitr2ri 292 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜃 ↔ 𝜑) | ||
Theorem | 3bitr3i 293 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜑 ↔ 𝜒) & ⊢ (𝜓 ↔ 𝜃) ⇒ ⊢ (𝜒 ↔ 𝜃) | ||
Theorem | 3bitr3ri 294 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜑 ↔ 𝜒) & ⊢ (𝜓 ↔ 𝜃) ⇒ ⊢ (𝜃 ↔ 𝜒) | ||
Theorem | 3bitr4i 295 | A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) ⇒ ⊢ (𝜒 ↔ 𝜃) | ||
Theorem | 3bitr4ri 296 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) ⇒ ⊢ (𝜃 ↔ 𝜒) | ||
Theorem | 3bitrd 297 | Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜏)) | ||
Theorem | 3bitrrd 298 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜓)) | ||
Theorem | 3bitr2d 299 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜏)) | ||
Theorem | 3bitr2rd 300 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |