| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > baib | Structured version Visualization version GIF 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 | baib.1 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
| 2 | ibar 528 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | |
| 3 | 1, 2 | bitr4id 290 | 1 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: baibr 536 ceqsrexbv 3656 elrab3 3693 dfpss3 4089 rabsn 4721 elrint2 4990 opres 6007 cores 6269 fnres 6695 fvres 6925 fvmpti 7015 f1ompt 7131 fliftfun 7332 isocnv3 7352 riotaxfrd 7422 ovid 7574 nlimon 7872 limom 7903 brdifun 8775 xpcomco 9102 0sdomg 9144 0sdomgOLD 9145 f1finf1o 9305 f1finf1oOLD 9306 ordtypelem9 9566 isacn 10084 alephinit 10135 isfin5-2 10431 pwfseqlem1 10698 pwfseqlem3 10700 pwfseqlem4 10702 ltresr 11180 xrlenlt 11326 znnnlt1 12644 difrp 13073 elfz 13553 fzolb2 13706 elfzo3 13716 fzouzsplit 13734 rabssnn0fi 14027 caubnd 15397 ello12 15552 elo12 15563 bitsval2 16462 smueqlem 16527 rpexp 16759 ramcl 17067 ismon2 17778 isepi2 17785 isfull2 17958 isfth2 17962 isghm3 19235 gastacos 19328 sylow2alem2 19636 lssnle 19692 isabl2 19808 submcmn2 19857 iscyggen2 19899 iscyg3 19904 cyggexb 19917 gsum2d2 19992 dprdw 20030 dprd2da 20062 iscrng2 20249 dvdsr2 20363 dfrhm2 20474 isdomn2 20711 isdomn2OLD 20712 sdrgacs 20802 islmhm3 21027 prmirredlem 21483 chrnzr 21545 iunocv 21699 iscss2 21704 ishil2 21739 obselocv 21748 psrbaglefi 21946 mplsubrglem 22024 bastop1 23000 isclo 23095 maxlp 23155 isperf2 23160 restperf 23192 cnpnei 23272 cnntr 23283 cnprest 23297 cnprest2 23298 lmres 23308 iscnrm2 23346 ist0-2 23352 ist1-2 23355 ishaus2 23359 tgcmp 23409 cmpfi 23416 dfconn2 23427 t1connperf 23444 subislly 23489 tx1cn 23617 tx2cn 23618 xkopt 23663 xkoinjcn 23695 ist0-4 23737 trfil2 23895 fin1aufil 23940 flimtopon 23978 elflim 23979 fclstopon 24020 isfcls2 24021 alexsubALTlem4 24058 ptcmplem3 24062 tgphaus 24125 xmetec 24444 prdsbl 24504 blval2 24575 isnvc2 24720 isnghm2 24745 isnmhm2 24773 0nmhm 24776 xrtgioo 24828 cncfcnvcn 24952 evth 24991 nmhmcn 25153 cmsss 25385 lssbn 25386 srabn 25394 ishl2 25404 ivthlem2 25487 0plef 25707 itg2monolem1 25785 itg2cnlem1 25796 itg2cnlem2 25797 ellimc2 25912 dvne0 26050 ellogdm 26681 dcubic 26889 atans2 26974 amgm 27034 ftalem3 27118 pclogsum 27259 dchrelbas3 27282 lgsabs1 27380 dchrvmaeq0 27548 rpvmasum2 27556 tgjustf 28481 clwwlkwwlksb 30073 ajval 30880 bnsscmcl 30887 axhcompl-zf 31017 seq1hcau 31206 hlim2 31211 issh3 31238 lnopcnre 32058 dmdbr2 32322 elatcv0 32360 iunsnima 32630 iunsnima2 32631 ecxpid 33389 ssdifidlprm 33486 ist0cld 33832 1stmbfm 34262 2ndmbfm 34263 eulerpartlemd 34368 oddprm2 34670 lfuhgr 35123 cvmlift2lem12 35319 bj-rest10 37089 topdifinfeq 37351 finxpsuclem 37398 curunc 37609 istotbnd2 37777 sstotbnd2 37781 isbnd3b 37792 totbndbnd 37796 br1cnvres 38270 ecres2 38280 fimgmcyc 42544 islnr2 43126 areaquad 43228 tfsconcat0i 43358 afv2res 47251 oddm1evenALTV 47662 oddp1evenALTV 47663 iscnrm3v 48850 isprsd 48852 joindm2 48865 meetdm2 48867 postcposALT 49172 postc 49173 |
| Copyright terms: Public domain | W3C validator |