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 6912 wfrlem5 7953 funsnfsupp 8851 sucprcreg 9059 fin23lem40 9767 ffz0iswrd 13885 s4f1o 14274 fsumsplitsnun 15104 lcmcllem 15934 lidldvgen 20022 mat1dimbas 21075 pmatcollpw3fi 21387 nbgrssvwo2 27138 wlkn0 27396 clwlkcompbp 27557 clwlkclwwlkflem 27776 konigsberglem5 28029 difininv 30273 prmidl2 30953 eulerpartlemgs2 31633 bnj1476 32114 bnj1204 32279 dfon2lem3 33025 frrlem13 33130 bj-ccinftydisj 34489 nninfnub 35020 ispridl2 35310 rp-isfinite6 39877 fnresfnco 43270 |
Copyright terms: Public domain | W3C validator |