![]() |
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 221 | . 2 ⊢ ((𝜓 ↔ 𝜃) ↔ (𝜃 ↔ 𝜓)) | |
4 | bicom 221 | . 2 ⊢ ((𝜒 ↔ 𝜃) ↔ (𝜃 ↔ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 313 | 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: bibi12d 345 bibi1 351 biass 385 axextg 2710 axextmo 2712 eqeq1dALT 2740 pm13.183 3616 elabgtOLD 3623 elrab3t 3642 mob 3673 reu6 3682 sbctt 3813 sbcabel 3832 isoeq2 7259 caovcang 7549 domunfican 9222 axacndlem4 10504 axacnd 10506 expeq0 13952 dfrtrclrec2 14903 relexpind 14909 sumodd 16230 prmdvdsexp 16551 isacs 17491 acsfn 17499 tsrlemax 18435 odeq 19291 isslw 19349 isabv 20231 t0sep 22627 xkopt 22958 kqt0lem 23039 r0sep 23051 nrmr0reg 23052 ismet 23628 isxmet 23629 stdbdxmet 23823 xrsxmet 24124 iccpnfcnv 24259 mdegle0 25394 isppw2 26416 tgjustf 27244 eleclclwwlkn 28849 eupth2lem1 28991 hvaddcan 29841 eigre 30606 opsbc2ie 31233 xrge0iifcnv 32326 sgn0bi 32959 signswch 32985 bnj1468 33270 subtr2 34725 nn0prpwlem 34732 nn0prpw 34733 bj-bm1.3ii 35473 dfgcd3 35733 ftc1anclem6 36094 zindbi 41179 expdioph 41256 islssfg2 41307 eliunov2 41862 pm14.122b 42614 elsetpreimafvbi 45484 line2ylem 46738 line2xlem 46740 |
Copyright terms: Public domain | W3C validator |