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 219, sylib 220, sylbir 237, sylibr 236; four inferences inferring an implication from two biconditionals: sylbb 221, sylbbr 238, sylbb1 239, sylbb2 240; four inferences inferring a biconditional from two biconditionals: bitri 277, bitr2i 278, bitr3i 279, bitr4i 280 (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 234, bitrd 281, syl5bb 285, syl6bb 289 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 230 | . 2 ⊢ (𝜒 → 𝜓) |
3 | sylbbr.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
4 | 2, 3 | sylibr 236 | 1 ⊢ (𝜒 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 |
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 209 |
This theorem is referenced by: bitri 277 euelss 4290 dfnfc2 4860 ndmima 5966 axcclem 9879 cshw1 14184 fsumcom2 15129 fprodcom2 15338 pmtr3ncomlem1 18601 mdetunilem7 21227 cmpcov2 21998 hausflf2 22606 umgredg 26923 vtxdginducedm1 27325 2pthfrgrrn 28061 eqdif 30281 cusgredgex2 32369 conway 33264 f1omptsnlem 34620 igenval2 35359 mpobi123f 35455 brtrclfv2 40092 clsk1indlem3 40413 or2expropbilem1 43287 |
Copyright terms: Public domain | W3C validator |