Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sylbb | Structured version Visualization version GIF version |
Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.) |
Ref | Expression |
---|---|
sylbb.1 | ⊢ (𝜑 ↔ 𝜓) |
sylbb.2 | ⊢ (𝜓 ↔ 𝜒) |
Ref | Expression |
---|---|
sylbb | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbb.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
2 | sylbb.2 | . . 3 ⊢ (𝜓 ↔ 𝜒) | |
3 | 2 | biimpi 206 | . 2 ⊢ (𝜓 → 𝜒) |
4 | 1, 3 | sylbi 207 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: bitri 264 ssdifim 3862 disjxiun 4649 trint 4768 pocl 5042 wefrc 5108 frsn 5189 ssrel 5207 funiun 6412 funopsn 6413 fissuni 8271 inf3lem2 8526 rankvalb 8660 xrrebnd 11999 xaddf 12055 elfznelfzob 12574 fsuppmapnn0ub 12795 hashinfxadd 13174 hashfun 13224 clatl 17116 sgrp2nmndlem5 17416 mat1dimelbas 20277 cfinfil 21697 dyadmax 23366 ausgrusgri 26063 nbupgrres 26266 usgredgsscusgredg 26355 1egrvtxdg0 26407 wlkp1lem7 26576 wwlksnfi 26801 isch3 28098 nmopun 28873 esumnul 30110 dya2iocnrect 30343 bnj849 30995 bnj1279 31086 bj-0int 33055 onsucuni3 33215 wl-nfeqfb 33323 poimirlem27 33436 unitresl 33884 iunrelexp0 37994 frege129d 38055 clsk3nimkb 38338 gneispace 38432 eliuniin 39279 eliuniin2 39303 stoweidlem48 40265 fourierdlem42 40366 fourierdlem80 40403 oddprmALTV 41598 alimp-no-surprise 42527 |
Copyright terms: Public domain | W3C validator |