| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > bibi1d | Structured version Visualization version GIF version | ||
| Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-1993.) |
| Ref | Expression |
|---|---|
| imbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| bibi1d | ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imbid.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | bibi2d 342 | . 2 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒))) |
| 3 | bicom 222 | . 2 ⊢ ((𝜓 ↔ 𝜃) ↔ (𝜃 ↔ 𝜓)) | |
| 4 | bicom 222 | . 2 ⊢ ((𝜒 ↔ 𝜃) ↔ (𝜃 ↔ 𝜒)) | |
| 5 | 2, 3, 4 | 3bitr4g 314 | 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: bibi12d 345 bibi1 351 biass 384 axextg 2710 axextmo 2712 eqeq1dALT 2740 pm13.183 3666 elrab3t 3691 mob 3723 reu6 3732 sbctt 3860 sbcabel 3878 isoeq2 7338 caovcang 7634 caofidlcan 7735 domunfican 9361 axacndlem4 10650 axacnd 10652 expeq0 14133 dfrtrclrec2 15097 relexpind 15103 sumodd 16425 prmdvdsexp 16752 isacs 17694 acsfn 17702 tsrlemax 18631 odeq 19568 isslw 19626 isabv 20812 t0sep 23332 xkopt 23663 kqt0lem 23744 r0sep 23756 nrmr0reg 23757 ismet 24333 isxmet 24334 stdbdxmet 24528 xrsxmet 24831 iccpnfcnv 24975 mdegle0 26116 isppw2 27158 tgjustf 28481 eleclclwwlkn 30095 eupth2lem1 30237 hvaddcan 31089 eigre 31854 opsbc2ie 32495 xrge0iifcnv 33932 sgn0bi 34550 signswch 34576 bnj1468 34860 axsepg2 35096 axsepg2ALT 35097 subtr2 36316 nn0prpwlem 36323 nn0prpw 36324 bj-bm1.3ii 37065 dfgcd3 37325 ftc1anclem6 37705 zindbi 42958 expdioph 43035 islssfg2 43083 eliunov2 43692 pm14.122b 44442 omssaxinf2 45005 elsetpreimafvbi 47378 line2ylem 48672 line2xlem 48674 |
| Copyright terms: Public domain | W3C validator |