| 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 216 | . 2 ⊢ (𝜓 → 𝜒) |
| 4 | 1, 3 | sylbi 217 | 1 ⊢ (𝜑 → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: bitri 275 elabgtOLD 3673 ssdifim 4273 ralf0 4514 disjxiun 5140 wefrc 5679 frsn 5773 ssrel 5792 ssrelOLD 5793 funiun 7167 funopsn 7168 ssfi 9213 enfii 9226 nneneq 9246 fissuni 9397 inf3lem2 9669 rankvalb 9837 djur 9959 xrrebnd 13210 xaddf 13266 elfznelfzob 13812 fsuppmapnn0ub 14036 hashinfxadd 14424 hashfun 14476 fz1f1o 15746 dvdszzq 16758 clatl 18553 sgrp2nmndlem5 18942 mat1dimelbas 22477 cfinfil 23901 dyadmax 25633 ausgrusgri 29185 nbupgrres 29381 usgredgsscusgredg 29477 1egrvtxdg0 29529 wlkp1lem7 29697 isch3 31260 nmopun 32033 2ndresdju 32659 cycpm2tr 33139 elrgspnlem1 33246 elrgspnlem2 33247 fldextrspunlsplem 33723 esumnul 34049 dya2iocnrect 34283 bnj849 34939 bnj1279 35032 cusgr3cyclex 35141 in-ax8 36225 bj-0int 37102 onsucuni3 37368 wl-nfeqfb 37537 poimirlem27 37654 sticksstones20 42167 fimgmcyclem 42543 sucomisnotcard 43557 iunrelexp0 43715 frege129d 43776 clsk3nimkb 44053 gneispace 44147 eliuniin 45104 eliuniin2 45125 stoweidlem48 46063 fourierdlem42 46164 fourierdlem80 46201 eubrdm 47048 oddprmALTV 47674 grtriproplem 47906 grtrif1o 47909 alimp-no-surprise 49300 |
| Copyright terms: Public domain | W3C validator |