| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sylbbr | Structured version Visualization version GIF version | ||
| Description: 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 217, sylib 218, sylbir 235, sylibr 234; four inferences inferring an implication from two biconditionals: sylbb 219, sylbbr 236, sylbb1 237, sylbb2 238; four inferences inferring a biconditional from two biconditionals: bitri 275, bitr2i 276, bitr3i 277, bitr4i 278 (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 232, bitrd 279, bitrid 283, bitrdi 287 and variants. (Contributed by BJ, 21-Apr-2019.) |
| Ref | Expression |
|---|---|
| sylbbr.1 | ⊢ (𝜑 ↔ 𝜓) |
| sylbbr.2 | ⊢ (𝜓 ↔ 𝜒) |
| Ref | Expression |
|---|---|
| sylbbr | ⊢ (𝜒 → 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sylbbr.2 | . . 3 ⊢ (𝜓 ↔ 𝜒) | |
| 2 | 1 | biimpri 228 | . 2 ⊢ (𝜒 → 𝜓) |
| 3 | sylbbr.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
| 4 | 2, 3 | sylibr 234 | 1 ⊢ (𝜒 → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 |
| This theorem is referenced by: bitri 275 euelss 4332 dfnfc2 4929 ndmima 6121 unfi 9211 axcclem 10497 cshw1 14860 fsumcom2 15810 fprodcom2 16020 pmtr3ncomlem1 19491 mdetunilem7 22624 cmpcov2 23398 hausflf2 24006 conway 27844 umgredg 29155 vtxdginducedm1 29561 2pthfrgrrn 30301 eqdif 32538 cusgredgex2 35128 f1omptsnlem 37337 igenval2 38073 mpobi123f 38169 brtrclfv2 43740 clsk1indlem3 44056 or2expropbilem1 47044 grtriproplem 47906 mo0sn 48735 |
| Copyright terms: Public domain | W3C validator |