![]() |
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 elabgtOLD 3658 ssdifim 4261 ralf0 4515 disjxiun 5146 poclOLD 5598 wefrc 5672 frsn 5765 ssrel 5784 ssrelOLD 5785 funiun 7156 funopsn 7157 ssfi 9198 enfii 9214 nneneq 9234 fissuni 9383 inf3lem2 9654 rankvalb 9822 djur 9944 xrrebnd 13182 xaddf 13238 elfznelfzob 13774 fsuppmapnn0ub 13996 hashinfxadd 14380 hashfun 14432 fz1f1o 15692 dvdszzq 16696 clatl 18503 sgrp2nmndlem5 18889 mat1dimelbas 22417 cfinfil 23841 dyadmax 25571 ausgrusgri 29053 nbupgrres 29249 usgredgsscusgredg 29345 1egrvtxdg0 29397 wlkp1lem7 29565 isch3 31123 nmopun 31896 2ndresdju 32516 cycpm2tr 32932 esumnul 33798 dya2iocnrect 34032 bnj849 34687 bnj1279 34780 cusgr3cyclex 34877 bj-0int 36711 onsucuni3 36977 wl-nfeqfb 37134 poimirlem27 37251 sticksstones20 41769 sucomisnotcard 43116 iunrelexp0 43274 frege129d 43335 clsk3nimkb 43612 gneispace 43706 eliuniin 44605 eliuniin2 44626 stoweidlem48 45574 fourierdlem42 45675 fourierdlem80 45712 eubrdm 46556 oddprmALTV 47164 alimp-no-surprise 48400 |
Copyright terms: Public domain | W3C validator |