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 874 elabgt 3596 ssdifim 4193 ralf0 4441 disjxiun 5067 poclOLD 5502 wefrc 5574 frsn 5665 ssrel 5683 funiun 7001 funopsn 7002 ssfi 8918 enfii 8932 fissuni 9054 inf3lem2 9317 rankvalb 9486 djur 9608 xrrebnd 12831 xaddf 12887 elfznelfzob 13421 fsuppmapnn0ub 13643 hashinfxadd 14028 hashfun 14080 fz1f1o 15350 clatl 18141 sgrp2nmndlem5 18483 mat1dimelbas 21528 cfinfil 22952 dyadmax 24667 ausgrusgri 27441 nbupgrres 27634 usgredgsscusgredg 27729 1egrvtxdg0 27781 wlkp1lem7 27949 isch3 29504 nmopun 30277 2ndresdju 30887 dvdszzq 31031 cycpm2tr 31288 esumnul 31916 dya2iocnrect 32148 bnj849 32805 bnj1279 32898 cusgr3cyclex 32998 bj-0int 35199 onsucuni3 35465 wl-nfeqfb 35622 poimirlem27 35731 sticksstones20 40050 iunrelexp0 41199 frege129d 41260 clsk3nimkb 41539 gneispace 41633 eliuniin 42538 eliuniin2 42558 stoweidlem48 43479 fourierdlem42 43580 fourierdlem80 43617 eubrdm 44417 oddprmALTV 45027 alimp-no-surprise 46371 |
Copyright terms: Public domain | W3C validator |