![]() |
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 2709 axextmo 2711 eqeq1dALT 2739 pm13.183 3616 elabgtOLD 3623 elrab3t 3642 mob 3673 reu6 3682 sbctt 3813 sbcabel 3832 isoeq2 7259 caovcang 7551 domunfican 9260 axacndlem4 10542 axacnd 10544 expeq0 13990 dfrtrclrec2 14935 relexpind 14941 sumodd 16262 prmdvdsexp 16583 isacs 17523 acsfn 17531 tsrlemax 18467 odeq 19323 isslw 19381 isabv 20263 t0sep 22659 xkopt 22990 kqt0lem 23071 r0sep 23083 nrmr0reg 23084 ismet 23660 isxmet 23661 stdbdxmet 23855 xrsxmet 24156 iccpnfcnv 24291 mdegle0 25426 isppw2 26448 tgjustf 27301 eleclclwwlkn 28906 eupth2lem1 29048 hvaddcan 29898 eigre 30663 opsbc2ie 31290 xrge0iifcnv 32383 sgn0bi 33016 signswch 33042 bnj1468 33327 subtr2 34754 nn0prpwlem 34761 nn0prpw 34762 bj-bm1.3ii 35502 dfgcd3 35762 ftc1anclem6 36123 zindbi 41208 expdioph 41285 islssfg2 41336 eliunov2 41893 pm14.122b 42645 elsetpreimafvbi 45515 line2ylem 46769 line2xlem 46771 |
Copyright terms: Public domain | W3C validator |