Theorem baib 914

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 507	. 2 |- ( ps -> ( ch <-> ( ps /\ ch ) ) )
2		baib.1	. 2 |- ( ph <-> ( ps /\ ch ) )
3	1, 2	syl6rbbr 268	1 |- ( ps -> ( ph <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  baibr  915  rbaibOLD  918  ceqsrexbv  3173  elrab3  3197  dfpss3  3519  rabsn  4039  elrint2  4277  elpredg  5394  fnres  5692  fvmpti  5947  f1ompt  6044  fliftfun  6205  isocnv3  6223  riotaxfrd  6282  ovid  6413  nlimon  6678  limom  6707  brdifun  7390  xpcomco  7662  0sdomg  7701  f1finf1o  7798  ordtypelem9  8041  isacn  8475  alephinit  8526  isfin5-2  8821  pwfseqlem1  9083  pwfseqlem3  9085  pwfseqlem4  9087  ltresr  9564  xrlenlt  9699  znnnlt1  10964  difrp  11337  elfz  11790  fzolb2  11927  elfzo3  11936  fzouzsplit  11953  rabssnn0fi  12198  caubnd  13421  ello12  13580  elo12  13591  bitsval2  14398  smueqlem  14464  rpexp  14672  ramcl  14987  ismon2  15639  isepi2  15646  isfull2  15816  isfth2  15820  isghm3  16884  gastacos  16964  sylow2alem2  17270  lssnle  17324  isabl2  17438  submcmn2  17479  iscyggen2  17516  iscyg3  17521  cyggexb  17533  gsum2d2  17606  dprdw  17642  dprd2da  17675  iscrng2  17796  dvdsr2  17875  dfrhm2  17945  islmhm3  18251  isdomn2  18523  psrbaglefi  18596  mplsubrglem  18663  prmirredlem  19064  chrnzr  19101  iunocv  19244  iscss2  19249  ishil2  19282  obselocv  19291  bastop1  20009  isclo  20103  maxlp  20163  isperf2  20168  restperf  20200  cnpnei  20280  cnntr  20291  cnprest  20305  cnprest2  20306  lmres  20316  iscnrm2  20354  ist0-2  20360  ist1-2  20363  ishaus2  20367  tgcmp  20416  cmpfi  20423  dfcon2  20434  t1conperf  20451  subislly  20496  tx1cn  20624  tx2cn  20625  xkopt  20670  xkoinjcn  20702  ist0-4  20744  trfil2  20902  fin1aufil  20947  flimtopon  20985  elflim  20986  fclstopon  21027  isfcls2  21028  alexsubALTlem4  21065  ptcmplem3  21069  tgphaus  21131  xmetec  21449  prdsbl  21506  blval2  21577  isnvc2  21701  isnghm2  21729  isnghm2OLD  21747  isnmhm2  21773  0nmhm  21776  xrtgioo  21824  cncfcnvcn  21953  evth  21987  nmhmcn  22134  cmsss  22318  lssbn  22319  srabn  22327  ishl2  22337  ivthlem2  22403  0plef  22630  itg2monolem1  22708  itg2cnlem1  22719  itg2cnlem2  22720  ellimc2  22832  dvne0  22963  ellogdm  23584  dcubic  23772  atans2  23857  amgm  23916  ftalem3  23999  pclogsum  24143  dchrelbas3  24166  lgsabs1  24262  dchrvmaeq0  24342  rpvmasum2  24350  ajval  26503  bnsscmcl  26510  axhcompl-zf  26651  seq1hcau  26840  hlim2  26845  issh3  26872  lnopcnre  27692  dmdbr2  27956  elatcv0  27994  iunsnima  28224  1stmbfm  29082  2ndmbfm  29083  eulerpartlemd  29199  cvmlift2lem12  30037  topdifinfeq  31753  finxpsuclem  31789  istotbnd2  32102  sstotbnd2  32106  isbnd3b  32117  totbndbnd  32121  islnr2  35973  sdrgacs  36067  areaquad  36101  oddm1evenALTV  38804  oddp1evenALTV  38805