![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > baibd | Structured version Visualization version Unicode version |
Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) |
Ref | Expression |
---|---|
baibd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
baibd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | baibd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ibar 511 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomd 206 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylan9bb 711 |
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 df-an 377 |
This theorem is referenced by: pw2f1olem 7663 eluz 11162 elicc4 11691 s111 12751 limsupgle 13546 lo1resb 13639 o1resb 13641 isercolllem2 13740 ismri2 15549 acsfiel2 15572 issect2 15670 eqglact 16879 eqgid 16880 cntzel 16988 dprdsubg 17668 subgdmdprd 17678 dprd2da 17686 dmdprdpr 17693 issubrg3 18047 ishil2 19293 obslbs 19304 iscld2 20054 isperf3 20180 cncnp2 20308 cnnei 20309 trfbas2 20869 flimrest 21009 flfnei 21017 fclsrest 21050 tsmssubm 21168 isnghm2 21740 isnghm3 21741 isnghm2OLD 21758 isnghm3OLD 21759 isnmhm2 21784 iscfil2 22247 caucfil 22264 ellimc2 22844 cnlimc 22855 lhop1 22978 dvfsumlem1 22990 fsumharmonic 23949 fsumvma 24153 fsumvma2 24154 vmasum 24156 chpchtsum 24159 chpub 24160 rpvmasum2 24362 dchrisum0lem1 24366 dirith 24379 cusgrauvtxb 25236 adjeu 27554 suppss3 28320 nndiffz1 28374 fsumcvg4 28763 qqhval2lem 28792 indpreima 28853 eulerpartlemf 29209 elorvc 29298 neibastop3 31024 relowlpssretop 31769 sstotbnd2 32108 isbnd3b 32119 lshpkr 32685 isat2 32855 islln4 33074 islpln4 33098 islvol4 33141 islhp2 33564 pw2f1o2val2 35897 rfcnpre1 37337 rfcnpre2 37349 uvtx2vtx1edg 39573 uvtx2vtx1edgb 39574 iscplgrnb 39586 |
Copyright terms: Public domain | W3C validator |