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 218 | . 2 ⊢ (𝜓 → 𝜒) |
4 | 1, 3 | sylbi 207 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: ftpg 6423 wfrlem5 7419 funsnfsupp 8299 fin23lem40 9173 s4f1o 13663 fsumsplitsnun 14484 fsumsplitsnunOLD 14486 lcmcllem 15309 mat1dimbas 20278 pmatcollpw3fi 20590 nbgrssvwo2 26261 wlkn0 26516 konigsberglem5 27118 eulerpartlemgs2 30442 bnj1476 30917 bnj1204 31080 dfon2lem3 31690 frrlem5 31784 bj-ccinftydisj 33100 nninfnub 33547 ispridl2 33837 rp-isfinite6 37864 fnresfnco 41206 |
Copyright terms: Public domain | W3C validator |