Theorem baib 944

Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)

Hypothesis

Ref	Expression
baib.1	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
baib	|- ( ps -> ( ph <-> ch ) )

Proof of Theorem baib

Step	Hyp	Ref	Expression
1		ibar 525	. 2 |- ( ps -> ( ch <-> ( ps /\ ch ) ) )
2		baib.1	. 2 |- ( ph <-> ( ps /\ ch ) )
3	1, 2	syl6rbbr 279	1 |- ( ps -> ( ph <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 386

This theorem is referenced by:  baibr  945  ceqsrexbv  3337  elrab3  3364  dfpss3  3693  rabsn  4256  elrint2  4519  elpredg  5694  fnres  6007  fvmpti  6281  f1ompt  6382  fliftfun  6562  isocnv3  6582  riotaxfrd  6642  ovid  6777  nlimon  7051  limom  7080  brdifun  7771  xpcomco  8050  0sdomg  8089  f1finf1o  8187  ordtypelem9  8431  isacn  8867  alephinit  8918  isfin5-2  9213  pwfseqlem1  9480  pwfseqlem3  9482  pwfseqlem4  9484  ltresr  9961  xrlenlt  10103  znnnlt1  11404  difrp  11868  elfz  12332  fzolb2  12477  elfzo3  12486  fzouzsplit  12503  rabssnn0fi  12785  caubnd  14098  ello12  14247  elo12  14258  bitsval2  15147  smueqlem  15212  rpexp  15432  ramcl  15733  ismon2  16394  isepi2  16401  isfull2  16571  isfth2  16575  isghm3  17661  gastacos  17743  sylow2alem2  18033  lssnle  18087  isabl2  18201  submcmn2  18244  iscyggen2  18283  iscyg3  18288  cyggexb  18300  gsum2d2  18373  dprdw  18409  dprd2da  18441  iscrng2  18563  dvdsr2  18647  dfrhm2  18717  islmhm3  19028  isdomn2  19299  psrbaglefi  19372  mplsubrglem  19439  prmirredlem  19841  chrnzr  19878  iunocv  20025  iscss2  20030  ishil2  20063  obselocv  20072  bastop1  20797  isclo  20891  maxlp  20951  isperf2  20956  restperf  20988  cnpnei  21068  cnntr  21079  cnprest  21093  cnprest2  21094  lmres  21104  iscnrm2  21142  ist0-2  21148  ist1-2  21151  ishaus2  21155  tgcmp  21204  cmpfi  21211  dfconn2  21222  t1connperf  21239  subislly  21284  tx1cn  21412  tx2cn  21413  xkopt  21458  xkoinjcn  21490  ist0-4  21532  trfil2  21691  fin1aufil  21736  flimtopon  21774  elflim  21775  fclstopon  21816  isfcls2  21817  alexsubALTlem4  21854  ptcmplem3  21858  tgphaus  21920  xmetec  22239  prdsbl  22296  blval2  22367  isnvc2  22503  isnghm2  22528  isnmhm2  22556  0nmhm  22559  xrtgioo  22609  cncfcnvcn  22724  evth  22758  nmhmcn  22920  cmsss  23147  lssbn  23148  srabn  23156  ishl2  23166  ivthlem2  23221  0plef  23439  itg2monolem1  23517  itg2cnlem1  23528  itg2cnlem2  23529  ellimc2  23641  dvne0  23774  ellogdm  24385  dcubic  24573  atans2  24658  amgm  24717  ftalem3  24801  pclogsum  24940  dchrelbas3  24963  lgsabs1  25061  dchrvmaeq0  25193  rpvmasum2  25201  ajval  27717  bnsscmcl  27724  axhcompl-zf  27855  seq1hcau  28044  hlim2  28049  issh3  28076  lnopcnre  28898  dmdbr2  29162  elatcv0  29200  iunsnima  29428  1stmbfm  30322  2ndmbfm  30323  eulerpartlemd  30428  oddprm2  30733  cvmlift2lem12  31296  bj-rest10  33041  topdifinfeq  33198  finxpsuclem  33234  curunc  33391  istotbnd2  33569  sstotbnd2  33573  isbnd3b  33584  totbndbnd  33588  ecres2  34044  islnr2  37684  sdrgacs  37771  areaquad  37802  oddm1evenALTV  41586  oddp1evenALTV  41587