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 230 | . 2 ⊢ (𝜓 → 𝜒) |
4 | 1, 3 | sylbi 219 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 |
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 209 |
This theorem is referenced by: ftpg 6911 wfrlem5 7951 funsnfsupp 8849 sucprcreg 9057 fin23lem40 9765 ffz0iswrd 13883 s4f1o 14272 fsumsplitsnun 15102 lcmcllem 15932 lidldvgen 20020 mat1dimbas 21073 pmatcollpw3fi 21385 nbgrssvwo2 27136 wlkn0 27394 clwlkcompbp 27555 clwlkclwwlkflem 27774 konigsberglem5 28027 difininv 30271 prmidl2 30951 eulerpartlemgs2 31631 bnj1476 32112 bnj1204 32277 dfon2lem3 33023 frrlem13 33128 bj-ccinftydisj 34487 nninfnub 35018 ispridl2 35308 rp-isfinite6 39875 fnresfnco 43267 |
Copyright terms: Public domain | W3C validator |