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: rexprg 4588 ftpg 6931 wfrlem5 7991 funsnfsupp 8933 sucprcreg 9141 fin23lem40 9854 ffz0iswrd 13985 s4f1o 14372 fsumsplitsnun 15206 lcmcllem 16040 catcone0 17064 lidldvgen 20150 mat1dimbas 21226 pmatcollpw3fi 21539 nbgrssvwo2 27307 wlkn0 27565 clwlkcompbp 27726 clwlkclwwlkflem 27944 konigsberglem5 28196 difininv 30441 prmidl2 31191 eulerpartlemgs2 31920 bnj1476 32401 bnj1204 32566 dfon2lem3 33338 frrlem13 33458 bj-ccinftydisj 35028 nninfnub 35555 ispridl2 35842 rp-isfinite6 40702 fnresfnco 44097 |
Copyright terms: Public domain | W3C validator |