![]() |
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 227 | . 2 ⊢ (𝜓 → 𝜒) |
4 | 1, 3 | sylbi 216 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: rexprg 4698 ftpg 7148 frrlem13 8277 wfrlem5OLD 8307 sdom0 9103 funsnfsupp 9382 sucprcreg 9591 fin23lem40 10341 ffz0iswrd 14486 s4f1o 14864 fsumsplitsnun 15696 lcmcllem 16528 catcone0 17626 lidldvgen 20879 mat1dimbas 21955 pmatcollpw3fi 22268 nbgrssvwo2 28598 wlkn0 28857 clwlkcompbp 29018 clwlkclwwlkflem 29236 konigsberglem5 29488 difininv 31732 prmidl2 32516 eulerpartlemgs2 33316 bnj1476 33795 bnj1204 33960 dfon2lem3 34694 bj-ccinftydisj 36031 nninfnub 36556 ispridl2 36843 rp-isfinite6 42201 fnresfnco 45685 |
Copyright terms: Public domain | W3C validator |