![]() |
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 2704 axextmo 2706 eqeq1dALT 2734 pm13.183 3652 elabgtOLD 3659 elrab3t 3678 mob 3709 reu6 3718 sbctt 3849 sbcabel 3868 isoeq2 7299 caovcang 7591 domunfican 9303 axacndlem4 10587 axacnd 10589 expeq0 14040 dfrtrclrec2 14987 relexpind 14993 sumodd 16313 prmdvdsexp 16634 isacs 17577 acsfn 17585 tsrlemax 18521 odeq 19382 isslw 19440 isabv 20376 t0sep 22757 xkopt 23088 kqt0lem 23169 r0sep 23181 nrmr0reg 23182 ismet 23758 isxmet 23759 stdbdxmet 23953 xrsxmet 24254 iccpnfcnv 24389 mdegle0 25524 isppw2 26546 tgjustf 27589 eleclclwwlkn 29194 eupth2lem1 29336 hvaddcan 30186 eigre 30951 opsbc2ie 31579 xrge0iifcnv 32744 sgn0bi 33377 signswch 33403 bnj1468 33688 subtr2 35004 nn0prpwlem 35011 nn0prpw 35012 bj-bm1.3ii 35749 dfgcd3 36009 ftc1anclem6 36370 zindbi 41456 expdioph 41533 islssfg2 41584 eliunov2 42201 pm14.122b 42953 elsetpreimafvbi 45831 line2ylem 47085 line2xlem 47087 |
Copyright terms: Public domain | W3C validator |