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 343 | . 2 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒))) |
3 | bicom 221 | . 2 ⊢ ((𝜓 ↔ 𝜃) ↔ (𝜃 ↔ 𝜓)) | |
4 | bicom 221 | . 2 ⊢ ((𝜒 ↔ 𝜃) ↔ (𝜃 ↔ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 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 346 bibi1 352 biass 386 axextg 2712 axextmo 2714 eqeq1dALT 2742 pm13.183 3598 elabgtOLD 3605 elrab3t 3624 mob 3653 reu6 3662 sbctt 3793 sbcabel 3812 isoeq2 7198 caovcang 7482 domunfican 9096 axacndlem4 10375 axacnd 10377 expeq0 13822 dfrtrclrec2 14778 relexpind 14784 sumodd 16106 prmdvdsexp 16429 isacs 17369 acsfn 17377 tsrlemax 18313 odeq 19167 isslw 19222 isabv 20088 t0sep 22484 xkopt 22815 kqt0lem 22896 r0sep 22908 nrmr0reg 22909 ismet 23485 isxmet 23486 stdbdxmet 23680 xrsxmet 23981 iccpnfcnv 24116 mdegle0 25251 isppw2 26273 tgjustf 26843 eleclclwwlkn 28449 eupth2lem1 28591 hvaddcan 29441 eigre 30206 opsbc2ie 30833 xrge0iifcnv 31892 sgn0bi 32523 signswch 32549 bnj1468 32835 subtr2 34513 nn0prpwlem 34520 nn0prpw 34521 bj-bm1.3ii 35244 dfgcd3 35504 ftc1anclem6 35864 zindbi 40775 expdioph 40852 islssfg2 40903 eliunov2 41294 pm14.122b 42048 elsetpreimafvbi 44854 line2ylem 46108 line2xlem 46110 |
Copyright terms: Public domain | W3C validator |