![]() |
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 530 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | bitr4id 290 | 1 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: baibr 538 ceqsrexbv 3643 elrab3 3683 dfpss3 4085 rabsn 4724 elrint2 4995 opres 5989 cores 6245 fnres 6674 fvres 6907 fvmpti 6993 f1ompt 7106 fliftfun 7304 isocnv3 7324 riotaxfrd 7395 ovid 7544 nlimon 7835 limom 7866 brdifun 8728 xpcomco 9058 0sdomg 9100 0sdomgOLD 9101 f1finf1o 9267 f1finf1oOLD 9268 ordtypelem9 9517 isacn 10035 alephinit 10086 isfin5-2 10382 pwfseqlem1 10649 pwfseqlem3 10651 pwfseqlem4 10653 ltresr 11131 xrlenlt 11275 znnnlt1 12585 difrp 13008 elfz 13486 fzolb2 13635 elfzo3 13645 fzouzsplit 13663 rabssnn0fi 13947 caubnd 15301 ello12 15456 elo12 15467 bitsval2 16362 smueqlem 16427 rpexp 16655 ramcl 16958 ismon2 17677 isepi2 17684 isfull2 17858 isfth2 17862 isghm3 19087 gastacos 19168 sylow2alem2 19479 lssnle 19535 isabl2 19651 submcmn2 19699 iscyggen2 19741 iscyg3 19746 cyggexb 19759 gsum2d2 19834 dprdw 19872 dprd2da 19904 iscrng2 20066 dvdsr2 20166 dfrhm2 20242 sdrgacs 20405 islmhm3 20627 isdomn2 20902 prmirredlem 21026 chrnzr 21066 iunocv 21218 iscss2 21223 ishil2 21258 obselocv 21267 psrbaglefi 21467 psrbaglefiOLD 21468 mplsubrglem 21545 bastop1 22478 isclo 22573 maxlp 22633 isperf2 22638 restperf 22670 cnpnei 22750 cnntr 22761 cnprest 22775 cnprest2 22776 lmres 22786 iscnrm2 22824 ist0-2 22830 ist1-2 22833 ishaus2 22837 tgcmp 22887 cmpfi 22894 dfconn2 22905 t1connperf 22922 subislly 22967 tx1cn 23095 tx2cn 23096 xkopt 23141 xkoinjcn 23173 ist0-4 23215 trfil2 23373 fin1aufil 23418 flimtopon 23456 elflim 23457 fclstopon 23498 isfcls2 23499 alexsubALTlem4 23536 ptcmplem3 23540 tgphaus 23603 xmetec 23922 prdsbl 23982 blval2 24053 isnvc2 24198 isnghm2 24223 isnmhm2 24251 0nmhm 24254 xrtgioo 24304 cncfcnvcn 24423 evth 24457 nmhmcn 24618 cmsss 24850 lssbn 24851 srabn 24859 ishl2 24869 ivthlem2 24951 0plef 25171 itg2monolem1 25250 itg2cnlem1 25261 itg2cnlem2 25262 ellimc2 25376 dvne0 25510 ellogdm 26129 dcubic 26331 atans2 26416 amgm 26475 ftalem3 26559 pclogsum 26698 dchrelbas3 26721 lgsabs1 26819 dchrvmaeq0 26987 rpvmasum2 26995 tgjustf 27704 clwwlkwwlksb 29287 ajval 30092 bnsscmcl 30099 axhcompl-zf 30229 seq1hcau 30418 hlim2 30423 issh3 30450 lnopcnre 31270 dmdbr2 31534 elatcv0 31572 iunsnima 31825 iunsnima2 31826 ecxpid 32441 ist0cld 32751 1stmbfm 33197 2ndmbfm 33198 eulerpartlemd 33303 oddprm2 33605 lfuhgr 34046 cvmlift2lem12 34243 bj-rest10 35907 topdifinfeq 36169 finxpsuclem 36216 curunc 36408 istotbnd2 36576 sstotbnd2 36580 isbnd3b 36591 totbndbnd 36595 br1cnvres 37075 ecres2 37085 islnr2 41789 areaquad 41898 tfsconcat0i 42028 afv2res 45882 oddm1evenALTV 46278 oddp1evenALTV 46279 iscnrm3v 47488 isprsd 47490 joindm2 47503 meetdm2 47505 postcposALT 47603 postc 47604 |
Copyright terms: Public domain | W3C validator |