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 529 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | |
2 | baib.1 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
3 | 1, 2 | syl6rbbr 291 | 1 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: baibr 537 ceqsrexbv 3647 elrab3 3678 dfpss3 4060 rabsn 4649 elrint2 4909 opres 5856 cores 6095 elpredg 6155 fnres 6467 fvres 6682 fvmpti 6760 f1ompt 6867 fliftfun 7054 isocnv3 7074 riotaxfrd 7137 ovid 7280 nlimon 7555 limom 7584 brdifun 8307 xpcomco 8595 0sdomg 8634 f1finf1o 8733 ordtypelem9 8978 isacn 9458 alephinit 9509 isfin5-2 9801 pwfseqlem1 10068 pwfseqlem3 10070 pwfseqlem4 10072 ltresr 10550 xrlenlt 10694 znnnlt1 11997 difrp 12415 elfz 12886 fzolb2 13033 elfzo3 13042 fzouzsplit 13060 rabssnn0fi 13342 caubnd 14706 ello12 14861 elo12 14872 bitsval2 15762 smueqlem 15827 rpexp 16052 ramcl 16353 ismon2 16992 isepi2 16999 isfull2 17169 isfth2 17173 isghm3 18297 gastacos 18378 sylow2alem2 18672 lssnle 18729 isabl2 18844 submcmn2 18888 iscyggen2 18929 iscyg3 18934 cyggexb 18948 gsum2d2 19023 dprdw 19061 dprd2da 19093 iscrng2 19242 dvdsr2 19326 dfrhm2 19398 sdrgacs 19509 islmhm3 19729 isdomn2 20000 psrbaglefi 20080 mplsubrglem 20147 prmirredlem 20568 chrnzr 20605 iunocv 20753 iscss2 20758 ishil2 20791 obselocv 20800 bastop1 21529 isclo 21623 maxlp 21683 isperf2 21688 restperf 21720 cnpnei 21800 cnntr 21811 cnprest 21825 cnprest2 21826 lmres 21836 iscnrm2 21874 ist0-2 21880 ist1-2 21883 ishaus2 21887 tgcmp 21937 cmpfi 21944 dfconn2 21955 t1connperf 21972 subislly 22017 tx1cn 22145 tx2cn 22146 xkopt 22191 xkoinjcn 22223 ist0-4 22265 trfil2 22423 fin1aufil 22468 flimtopon 22506 elflim 22507 fclstopon 22548 isfcls2 22549 alexsubALTlem4 22586 ptcmplem3 22590 tgphaus 22652 xmetec 22971 prdsbl 23028 blval2 23099 isnvc2 23235 isnghm2 23260 isnmhm2 23288 0nmhm 23291 xrtgioo 23341 cncfcnvcn 23456 evth 23490 nmhmcn 23651 cmsss 23881 lssbn 23882 srabn 23890 ishl2 23900 ivthlem2 23980 0plef 24200 itg2monolem1 24278 itg2cnlem1 24289 itg2cnlem2 24290 ellimc2 24402 dvne0 24535 ellogdm 25149 dcubic 25351 atans2 25436 amgm 25495 ftalem3 25579 pclogsum 25718 dchrelbas3 25741 lgsabs1 25839 dchrvmaeq0 26007 rpvmasum2 26015 tgjustf 26186 clwwlkwwlksb 27760 ajval 28565 bnsscmcl 28572 axhcompl-zf 28702 seq1hcau 28891 hlim2 28896 issh3 28923 lnopcnre 29743 dmdbr2 30007 elatcv0 30045 iunsnima 30297 ecxpid 30852 1stmbfm 31417 2ndmbfm 31418 eulerpartlemd 31523 oddprm2 31825 lfuhgr 32261 cvmlift2lem12 32458 bj-rest10 34273 topdifinfeq 34513 finxpsuclem 34560 curunc 34755 istotbnd2 34929 sstotbnd2 34933 isbnd3b 34944 totbndbnd 34948 ecres2 35417 islnr2 39592 areaquad 39701 afv2res 43315 oddm1evenALTV 43717 oddp1evenALTV 43718 |
Copyright terms: Public domain | W3C validator |