![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > baib | Structured version Visualization version Unicode version |
Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.) |
Ref | Expression |
---|---|
baib.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
baib |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ibar 507 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | baib.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6rbbr 268 |
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 189 df-an 373 |
This theorem is referenced by: baibr 915 rbaibOLD 918 ceqsrexbv 3173 elrab3 3197 dfpss3 3519 rabsn 4039 elrint2 4277 elpredg 5394 fnres 5692 fvmpti 5947 f1ompt 6044 fliftfun 6205 isocnv3 6223 riotaxfrd 6282 ovid 6413 nlimon 6678 limom 6707 brdifun 7390 xpcomco 7662 0sdomg 7701 f1finf1o 7798 ordtypelem9 8041 isacn 8475 alephinit 8526 isfin5-2 8821 pwfseqlem1 9083 pwfseqlem3 9085 pwfseqlem4 9087 ltresr 9564 xrlenlt 9699 znnnlt1 10964 difrp 11337 elfz 11790 fzolb2 11927 elfzo3 11936 fzouzsplit 11953 rabssnn0fi 12198 caubnd 13421 ello12 13580 elo12 13591 bitsval2 14398 smueqlem 14464 rpexp 14672 ramcl 14987 ismon2 15639 isepi2 15646 isfull2 15816 isfth2 15820 isghm3 16884 gastacos 16964 sylow2alem2 17270 lssnle 17324 isabl2 17438 submcmn2 17479 iscyggen2 17516 iscyg3 17521 cyggexb 17533 gsum2d2 17606 dprdw 17642 dprd2da 17675 iscrng2 17796 dvdsr2 17875 dfrhm2 17945 islmhm3 18251 isdomn2 18523 psrbaglefi 18596 mplsubrglem 18663 prmirredlem 19064 chrnzr 19101 iunocv 19244 iscss2 19249 ishil2 19282 obselocv 19291 bastop1 20009 isclo 20103 maxlp 20163 isperf2 20168 restperf 20200 cnpnei 20280 cnntr 20291 cnprest 20305 cnprest2 20306 lmres 20316 iscnrm2 20354 ist0-2 20360 ist1-2 20363 ishaus2 20367 tgcmp 20416 cmpfi 20423 dfcon2 20434 t1conperf 20451 subislly 20496 tx1cn 20624 tx2cn 20625 xkopt 20670 xkoinjcn 20702 ist0-4 20744 trfil2 20902 fin1aufil 20947 flimtopon 20985 elflim 20986 fclstopon 21027 isfcls2 21028 alexsubALTlem4 21065 ptcmplem3 21069 tgphaus 21131 xmetec 21449 prdsbl 21506 blval2 21577 isnvc2 21701 isnghm2 21729 isnghm2OLD 21747 isnmhm2 21773 0nmhm 21776 xrtgioo 21824 cncfcnvcn 21953 evth 21987 nmhmcn 22134 cmsss 22318 lssbn 22319 srabn 22327 ishl2 22337 ivthlem2 22403 0plef 22630 itg2monolem1 22708 itg2cnlem1 22719 itg2cnlem2 22720 ellimc2 22832 dvne0 22963 ellogdm 23584 dcubic 23772 atans2 23857 amgm 23916 ftalem3 23999 pclogsum 24143 dchrelbas3 24166 lgsabs1 24262 dchrvmaeq0 24342 rpvmasum2 24350 ajval 26503 bnsscmcl 26510 axhcompl-zf 26651 seq1hcau 26840 hlim2 26845 issh3 26872 lnopcnre 27692 dmdbr2 27956 elatcv0 27994 iunsnima 28224 1stmbfm 29082 2ndmbfm 29083 eulerpartlemd 29199 cvmlift2lem12 30037 topdifinfeq 31753 finxpsuclem 31789 istotbnd2 32102 sstotbnd2 32106 isbnd3b 32117 totbndbnd 32121 islnr2 35973 sdrgacs 36067 areaquad 36101 oddm1evenALTV 38804 oddp1evenALTV 38805 |
Copyright terms: Public domain | W3C validator |