![]() |
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 3895 disjxiun 4681 trint 4801 pocl 5071 wefrc 5137 frsn 5223 ssrel 5241 funiun 6452 funopsn 6453 fissuni 8312 inf3lem2 8564 rankvalb 8698 xrrebnd 12037 xaddf 12093 elfznelfzob 12614 fsuppmapnn0ub 12835 hashinfxadd 13212 hashfun 13262 fz1f1o 14485 clatl 17163 sgrp2nmndlem5 17463 mat1dimelbas 20325 cfinfil 21744 dyadmax 23412 ausgrusgri 26108 nbupgrres 26310 usgredgsscusgredg 26411 1egrvtxdg0 26463 wlkp1lem7 26632 wwlksnfi 26869 isch3 28226 nmopun 29001 esumnul 30238 dya2iocnrect 30471 bnj849 31121 bnj1279 31212 bj-0int 33180 onsucuni3 33345 wl-nfeqfb 33453 poimirlem27 33566 unitresl 34014 iunrelexp0 38311 frege129d 38372 clsk3nimkb 38655 gneispace 38749 eliuniin 39593 eliuniin2 39617 stoweidlem48 40583 fourierdlem42 40684 fourierdlem80 40721 oddprmALTV 41923 alimp-no-surprise 42855 |
Copyright terms: Public domain | W3C validator |