![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bibi1d | Structured version Visualization version Unicode 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 324 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | bicom 205 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | bicom 205 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3bitr4g 296 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 |
This theorem is referenced by: bibi12d 327 bibi1 333 biass 365 eubid 2327 axext3 2443 axext3ALT 2444 bm1.1 2446 eqeq1dALT 2464 pm13.183 3190 elabgt 3193 elrab3t 3206 mob 3231 sbctt 3341 sbcabel 3356 isoeq2 6235 caovcang 6496 domunfican 7869 axacndlem4 9060 axacnd 9062 expeq0 12333 dfrtrclrec2 13168 relexpind 13175 prmdvdsexp 14715 isacs 15605 acsfn 15613 tsrlemax 16514 odeq 17247 isslw 17308 isabv 18095 t0sep 20388 xkopt 20718 kqt0lem 20799 r0sep 20811 nrmr0reg 20812 ismet 21386 isxmet 21387 stdbdxmet 21578 xrsxmet 21875 iccpnfcnv 22020 mdegle0 23074 isppw2 24090 cusgrauvtxb 25272 eleclclwwlkn 25609 eupath2lem1 25753 hvaddcan 26771 eigre 27536 xrge0iifcnv 28787 sgn0bi 29466 signswch 29498 bnj1468 29705 br1steqg 30464 br2ndeqg 30465 subtr2 31019 nn0prpwlem 31026 nn0prpw 31027 bj-axext3 31428 ftc1anclem6 32066 zindbi 35838 expdioph 35922 islssfg2 35973 eliunov2 36315 pm14.122b 36817 |
Copyright terms: Public domain | W3C validator |