| 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 228 | . 2 ⊢ (𝜓 → 𝜒) |
| 4 | 1, 3 | sylbi 217 | 1 ⊢ (𝜑 → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: rexprg 4697 ftpg 7176 frrlem13 8323 wfrlem5OLD 8353 brinxper 8774 sdom0 9148 funsnfsupp 9432 sucprcreg 9641 fin23lem40 10391 ffz0iswrd 14579 s4f1o 14957 fsumsplitsnun 15791 lcmcllem 16633 catcone0 17730 lidldvgen 21344 mat1dimbas 22478 pmatcollpw3fi 22791 nbgrssvwo2 29379 wlkn0 29639 clwlkcompbp 29802 clwlkclwwlkflem 30023 konigsberglem5 30275 difininv 32536 prmidl2 33469 eulerpartlemgs2 34382 bnj1476 34861 bnj1204 35026 dfon2lem3 35786 bj-ccinftydisj 37214 nninfnub 37758 ispridl2 38045 rp-isfinite6 43531 fnresfnco 47053 |
| Copyright terms: Public domain | W3C validator |