![]() |
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 331 | . 2 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒))) |
3 | bicom 212 | . 2 ⊢ ((𝜓 ↔ 𝜃) ↔ (𝜃 ↔ 𝜓)) | |
4 | bicom 212 | . 2 ⊢ ((𝜒 ↔ 𝜃) ↔ (𝜃 ↔ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 303 | 1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: bibi12d 334 bibi1 340 biass 373 eubid 2625 axext3 2742 axext3ALT 2743 bm1.1 2745 eqeq1dALT 2763 pm13.183 3484 elabgt 3487 elrab3t 3503 mob 3529 reu6 3536 sbctt 3641 sbcabel 3658 isoeq2 6731 caovcang 7000 domunfican 8398 axacndlem4 9624 axacnd 9626 expeq0 13084 dfrtrclrec2 13996 relexpind 14003 sumodd 15313 prmdvdsexp 15629 isacs 16513 acsfn 16521 tsrlemax 17421 odeq 18169 isslw 18223 isabv 19021 t0sep 21330 xkopt 21660 kqt0lem 21741 r0sep 21753 nrmr0reg 21754 ismet 22329 isxmet 22330 stdbdxmet 22521 xrsxmet 22813 iccpnfcnv 22944 mdegle0 24036 isppw2 25040 eleclclwwlkn 27207 eupth2lem1 27370 hvaddcan 28236 eigre 29003 xrge0iifcnv 30288 sgn0bi 30918 signswch 30947 bnj1468 31223 br1steqgOLD 31979 br2ndeqgOLD 31980 subtr2 32615 nn0prpwlem 32623 nn0prpw 32624 bj-axext3 33075 dfgcd3 33481 ftc1anclem6 33803 zindbi 38013 expdioph 38092 islssfg2 38143 eliunov2 38473 pm14.122b 39126 |
Copyright terms: Public domain | W3C validator |