| 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 219 | . 2 ⊢ (𝜓 → 𝜒) |
| 4 | 1, 3 | sylbi 220 | 1 ⊢ (𝜑 → 𝜒) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This proof depends on definitions: df-bi 210 |
| This theorem is used by: bitri 278 ssdifim 4229 disjxiun 5111 wefrc 5660 frsn 5754 ssrel 5774 funiun 7150 funopsn 7151 funopsnOLD 7152 ssfi 9167 enfii 9180 nneneq 9200 fissuni 9324 inf3lem2 9608 rankvalb 9779 djur 9924 xrrebnd 13212 xaddf 13268 elfznelfzob 13822 fsuppmapnn0ub 14051 hashinfxadd 14441 hashfun 14494 fz1f1o 15787 dvdszzq 16805 clatl 18589 sgrp2nmndlem5 19022 mat1dimelbas 22665 cfinfil 24087 dyadmax 25794 ausgrusgri 29555 nbupgrres 29751 usgredgsscusgredg 29846 1egrvtxdg0 29898 wlkp1lem7 30064 isch3 31630 nmopun 32403 2ndresdju 33031 cycpm2tr 33470 elrgspnlem1 33593 elrgspnlem2 33594 fldextrspunlsplem 34094 esumnul 34469 dya2iocnrect 34703 bnj849 35345 bnj1279 35438 rankscott 35546 cusgr3cyclex 35649 in-ax8 36777 regsfromunir1 37092 bj-vn0ALT 37749 bj-0int 37784 onsucuni3 38054 wl-nfeqfb 38232 poimirlem27 38339 sticksstones20 42974 fimgmcyclem 43342 sucomisnotcard 44311 iunrelexp0 44469 frege129d 44530 clsk3nimkb 44807 gneispace 44901 eliuniin 45858 eliuniin2 45879 stoweidlem48 46803 fourierdlem42 46904 fourierdlem80 46941 eubrdm 47814 oddprmALTV 48493 grtriproplem 48745 grtrif1o 48748 pgnbgreunbgr 48931 alimp-no-surprise 50600 |
| Copyright terms: Public domain | W3C validator |