![]() |
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 215 | . 2 ⊢ (𝜓 → 𝜒) |
4 | 1, 3 | sylbi 216 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: bitri 274 unitreslOLD 876 elabgt 3624 ssdifim 4222 ralf0 4471 disjxiun 5102 poclOLD 5553 wefrc 5627 frsn 5719 ssrel 5738 ssrelOLD 5739 funiun 7092 funopsn 7093 ssfi 9116 enfii 9132 nneneq 9152 fissuni 9300 inf3lem2 9564 rankvalb 9732 djur 9854 xrrebnd 13086 xaddf 13142 elfznelfzob 13677 fsuppmapnn0ub 13899 hashinfxadd 14284 hashfun 14336 fz1f1o 15594 clatl 18396 sgrp2nmndlem5 18738 mat1dimelbas 21818 cfinfil 23242 dyadmax 24960 ausgrusgri 28066 nbupgrres 28259 usgredgsscusgredg 28354 1egrvtxdg0 28406 wlkp1lem7 28574 isch3 30130 nmopun 30903 2ndresdju 31512 dvdszzq 31655 cycpm2tr 31912 esumnul 32587 dya2iocnrect 32821 bnj849 33477 bnj1279 33570 cusgr3cyclex 33670 bj-0int 35562 onsucuni3 35828 wl-nfeqfb 35985 poimirlem27 36095 sticksstones20 40564 sucomisnotcard 41797 iunrelexp0 41955 frege129d 42016 clsk3nimkb 42293 gneispace 42387 eliuniin 43290 eliuniin2 43311 stoweidlem48 44260 fourierdlem42 44361 fourierdlem80 44398 eubrdm 45241 oddprmALTV 45850 alimp-no-surprise 47199 |
Copyright terms: Public domain | W3C validator |