![]() |
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 231 | . 2 ⊢ (𝜓 → 𝜒) |
4 | 1, 3 | sylbi 220 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 |
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 210 |
This theorem is referenced by: ftpg 6895 wfrlem5 7942 funsnfsupp 8841 sucprcreg 9049 fin23lem40 9762 ffz0iswrd 13884 s4f1o 14271 fsumsplitsnun 15102 lcmcllem 15930 lidldvgen 20021 mat1dimbas 21077 pmatcollpw3fi 21390 nbgrssvwo2 27152 wlkn0 27410 clwlkcompbp 27571 clwlkclwwlkflem 27789 konigsberglem5 28041 difininv 30288 prmidl2 31024 eulerpartlemgs2 31748 bnj1476 32229 bnj1204 32394 dfon2lem3 33143 frrlem13 33248 bj-ccinftydisj 34628 nninfnub 35189 ispridl2 35476 rp-isfinite6 40226 fnresfnco 43633 |
Copyright terms: Public domain | W3C validator |