Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sylbb2 | Structured version Visualization version GIF version |
Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.) |
Ref | Expression |
---|---|
sylbb2.1 | ⊢ (𝜑 ↔ 𝜓) |
sylbb2.2 | ⊢ (𝜒 ↔ 𝜓) |
Ref | Expression |
---|---|
sylbb2 | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbb2.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
2 | sylbb2.2 | . . 3 ⊢ (𝜒 ↔ 𝜓) | |
3 | 2 | biimpri 217 | . 2 ⊢ (𝜓 → 𝜒) |
4 | 1, 3 | sylbi 206 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: ftpg 6328 wfrlem5 7306 funsnfsupp 8182 fin23lem40 9056 s4f1o 13513 fsumsplitsnun 14328 lcmcllem 15147 mat1dimbas 20097 pmatcollpw3fi 20409 usgrarnedg 25913 nbgrassvwo 25966 nbgrassvwo2 25967 nbcusgra 25992 wwlknndef 26265 clwwlknndef 26301 eulerpartlemgs2 29769 bnj1476 30171 bnj1204 30334 dfon2lem3 30934 frrlem5 31028 bj-ccinftydisj 32277 nninfnub 32717 ispridl2 33007 rp-isfinite6 36883 fnresfnco 39855 nbgrssvwo2 40587 1wlkn0 40825 konigsberglem5 41426 |
Copyright terms: Public domain | W3C validator |