Theorem baib 901

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  baibr  902  rbaibOLD  905  ceqsrexbv  3238  elrab3  3262  dfpss3  3590  rabsn  4094  elrint2  4324  fnres  5697  fvmpti  5949  f1ompt  6043  fliftfun  6198  isocnv3  6216  riotaxfrd  6276  ovid  6403  nlimon  6670  limom  6699  brdifun  7338  xpcomco  7607  0sdomg  7646  f1finf1o  7746  ordtypelem9  7951  isacn  8425  alephinit  8476  isfin5-2  8771  pwfseqlem1  9036  pwfseqlem3  9038  pwfseqlem4  9040  ltresr  9517  xrlenlt  9652  znnnlt1  10891  difrp  11253  elfz  11678  fzolb2  11803  elfzo3  11812  fzouzsplit  11828  rabssnn0fi  12063  caubnd  13154  ello12  13302  elo12  13313  bitsval2  13934  smueqlem  13999  rpexp  14120  ramcl  14406  ismon2  14990  isepi2  14997  isfull2  15138  isfth2  15142  isghm3  16073  gastacos  16153  sylow2alem2  16444  lssnle  16498  isabl2  16612  submcmn2  16650  iscyggen2  16687  iscyg3  16692  cyggexb  16704  gsum2d2  16805  dprdw  16846  dprdwOLD  16852  dprd2da  16893  iscrng2  17015  dvdsr2  17097  dfrhm2  17167  islmhm3  17474  isdomn2  17747  psrbaglefi  17822  psrbaglefiOLD  17823  mplsubrglem  17899  mplsubrglemOLD  17900  prmirredlem  18318  prmirredlemOLD  18321  chrnzr  18362  iunocv  18507  iscss2  18512  ishil2  18545  obselocv  18554  bastop1  19289  isclo  19382  maxlp  19442  isperf2  19447  restperf  19479  cnpnei  19559  cnntr  19570  cnprest  19584  cnprest2  19585  lmres  19595  iscnrm2  19633  ist0-2  19639  ist1-2  19642  ishaus2  19646  tgcmp  19695  cmpfi  19702  dfcon2  19714  t1conperf  19731  subislly  19776  tx1cn  19873  tx2cn  19874  xkopt  19919  xkoinjcn  19951  ist0-4  19993  trfil2  20151  fin1aufil  20196  flimtopon  20234  elflim  20235  fclstopon  20276  isfcls2  20277  alexsubALTlem4  20313  ptcmplem3  20317  tgphaus  20378  xmetec  20700  prdsbl  20757  blval2  20841  isnvc2  20970  isnghm2  20994  isnmhm2  21022  0nmhm  21025  xrtgioo  21074  cncfcnvcn  21188  evth  21222  nmhmcn  21366  cmsss  21552  lssbn  21553  srabn  21563  ishl2  21573  ivthlem2  21627  0plef  21842  itg2monolem1  21920  itg2cnlem1  21931  itg2cnlem2  21932  ellimc2  22044  dvne0  22175  ellogdm  22776  dcubic  22933  atans2  23018  amgm  23076  ftalem3  23104  pclogsum  23246  dchrelbas3  23269  lgsabs1  23365  dchrvmaeq0  23445  rpvmasum2  23453  ebtwntg  23989  ajval  25481  bnsscmcl  25488  axhcompl-zf  25619  seq1hcau  25808  hlim2  25813  issh3  25841  lnopcnre  26662  dmdbr2  26926  elatcv0  26964  1stmbfm  27899  2ndmbfm  27900  eulerpartlemd  27973  cvmlift2lem12  28427  elpredg  28863  istotbnd2  29897  sstotbnd2  29901  isbnd3b  29912  totbndbnd  29916  islnr2  30695  sdrgacs  30783  areaquad  30817