| 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 4659 ftpg 7143 frrlem13 8283 brinxper 8712 sdom0 9085 funsnfsupp 9340 sucprcreg 9556 sucprcregOLD 9557 fin23lem40 10323 ffz0iswrd 14566 s4f1o 14943 fsumsplitsnun 15794 lcmcllem 16642 catcone0 17731 prmidl2 21425 lidldvgen 21459 mat1dimbas 22586 pmatcollpw3fi 22899 nbgrssvwo2 29617 wlkn0 29875 clwlkcompbp 30036 clwlkclwwlkflem 30260 konigsberglem5 30512 difininv 32769 eulerpartlemgs2 34682 bnj1476 35147 bnj1204 35312 axprALT2 35412 noinfepregs 35436 dfon2lem3 36141 bj-ccinftydisj 37712 nninfnub 38257 ispridl2 38544 rp-isfinite6 44101 fnresfnco 47634 |
| Copyright terms: Public domain | W3C validator |