![]() |
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 | ibar 518 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | |
2 | baib.1 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
3 | 1, 2 | syl6rbbr 279 | 1 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 |
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 197 df-an 383 |
This theorem is referenced by: baibr 526 ceqsrexbv 3487 elrab3 3516 dfpss3 3843 rabsn 4392 elrint2 4653 elpredg 5835 fnres 6145 fvmpti 6421 f1ompt 6522 fliftfun 6703 isocnv3 6723 riotaxfrd 6783 ovid 6922 nlimon 7196 limom 7225 brdifun 7923 xpcomco 8204 0sdomg 8243 f1finf1o 8341 ordtypelem9 8585 isacn 9065 alephinit 9116 isfin5-2 9413 pwfseqlem1 9680 pwfseqlem3 9682 pwfseqlem4 9684 ltresr 10161 xrlenlt 10303 znnnlt1 11604 difrp 12064 elfz 12532 fzolb2 12678 elfzo3 12687 fzouzsplit 12704 rabssnn0fi 12986 caubnd 14299 ello12 14448 elo12 14459 bitsval2 15348 smueqlem 15413 rpexp 15632 ramcl 15933 ismon2 16594 isepi2 16601 isfull2 16771 isfth2 16775 isghm3 17862 gastacos 17943 sylow2alem2 18233 lssnle 18287 isabl2 18401 submcmn2 18444 iscyggen2 18483 iscyg3 18488 cyggexb 18500 gsum2d2 18573 dprdw 18610 dprd2da 18642 iscrng2 18764 dvdsr2 18848 dfrhm2 18920 islmhm3 19234 isdomn2 19507 psrbaglefi 19580 mplsubrglem 19647 prmirredlem 20049 chrnzr 20086 iunocv 20235 iscss2 20240 ishil2 20273 obselocv 20282 bastop1 21011 isclo 21105 maxlp 21165 isperf2 21170 restperf 21202 cnpnei 21282 cnntr 21293 cnprest 21307 cnprest2 21308 lmres 21318 iscnrm2 21356 ist0-2 21362 ist1-2 21365 ishaus2 21369 tgcmp 21418 cmpfi 21425 dfconn2 21436 t1connperf 21453 subislly 21498 tx1cn 21626 tx2cn 21627 xkopt 21672 xkoinjcn 21704 ist0-4 21746 trfil2 21904 fin1aufil 21949 flimtopon 21987 elflim 21988 fclstopon 22029 isfcls2 22030 alexsubALTlem4 22067 ptcmplem3 22071 tgphaus 22133 xmetec 22452 prdsbl 22509 blval2 22580 isnvc2 22716 isnghm2 22741 isnmhm2 22769 0nmhm 22772 xrtgioo 22822 cncfcnvcn 22937 evth 22971 nmhmcn 23132 cmsss 23359 lssbn 23360 srabn 23368 ishl2 23378 ivthlem2 23433 0plef 23652 itg2monolem1 23730 itg2cnlem1 23741 itg2cnlem2 23742 ellimc2 23854 dvne0 23987 ellogdm 24599 dcubic 24787 atans2 24872 amgm 24931 ftalem3 25015 pclogsum 25154 dchrelbas3 25177 lgsabs1 25275 dchrvmaeq0 25407 rpvmasum2 25415 clwwlkwwlksb 27204 ajval 28050 bnsscmcl 28057 axhcompl-zf 28188 seq1hcau 28377 hlim2 28382 issh3 28409 lnopcnre 29231 dmdbr2 29495 elatcv0 29533 iunsnima 29761 1stmbfm 30655 2ndmbfm 30656 eulerpartlemd 30761 oddprm2 31066 cvmlift2lem12 31627 bj-rest10 33366 topdifinfeq 33528 finxpsuclem 33564 curunc 33717 istotbnd2 33894 sstotbnd2 33898 isbnd3b 33909 totbndbnd 33913 ecres2 34380 islnr2 38203 sdrgacs 38290 areaquad 38321 oddm1evenALTV 42107 oddp1evenALTV 42108 |
Copyright terms: Public domain | W3C validator |