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 502	. 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 367

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 369

This theorem is referenced by:  baibr  902  rbaibOLD  905  ceqsrexbv  3231  elrab3  3255  dfpss3  3576  rabsn  4083  elrint2  4314  fnres  5679  fvmpti  5930  f1ompt  6029  fliftfun  6185  isocnv3  6203  riotaxfrd  6262  ovid  6392  nlimon  6659  limom  6688  brdifun  7330  xpcomco  7600  0sdomg  7639  f1finf1o  7739  ordtypelem9  7943  isacn  8416  alephinit  8467  isfin5-2  8762  pwfseqlem1  9025  pwfseqlem3  9027  pwfseqlem4  9029  ltresr  9506  xrlenlt  9641  znnnlt1  10887  difrp  11255  elfz  11681  fzolb2  11811  elfzo3  11820  fzouzsplit  11837  rabssnn0fi  12077  caubnd  13273  ello12  13421  elo12  13432  bitsval2  14159  smueqlem  14224  rpexp  14345  ramcl  14631  ismon2  15222  isepi2  15229  isfull2  15399  isfth2  15403  isghm3  16467  gastacos  16547  sylow2alem2  16837  lssnle  16891  isabl2  17005  submcmn2  17046  iscyggen2  17083  iscyg3  17088  cyggexb  17100  gsum2d2  17198  dprdw  17238  dprdwOLD  17245  dprd2da  17286  iscrng2  17409  dvdsr2  17491  dfrhm2  17561  islmhm3  17869  isdomn2  18143  psrbaglefi  18218  psrbaglefiOLD  18219  mplsubrglem  18295  mplsubrglemOLD  18296  prmirredlem  18705  chrnzr  18742  iunocv  18885  iscss2  18890  ishil2  18923  obselocv  18932  bastop1  19662  isclo  19755  maxlp  19815  isperf2  19820  restperf  19852  cnpnei  19932  cnntr  19943  cnprest  19957  cnprest2  19958  lmres  19968  iscnrm2  20006  ist0-2  20012  ist1-2  20015  ishaus2  20019  tgcmp  20068  cmpfi  20075  dfcon2  20086  t1conperf  20103  subislly  20148  tx1cn  20276  tx2cn  20277  xkopt  20322  xkoinjcn  20354  ist0-4  20396  trfil2  20554  fin1aufil  20599  flimtopon  20637  elflim  20638  fclstopon  20679  isfcls2  20680  alexsubALTlem4  20716  ptcmplem3  20720  tgphaus  20781  xmetec  21103  prdsbl  21160  blval2  21244  isnvc2  21373  isnghm2  21397  isnmhm2  21425  0nmhm  21428  xrtgioo  21477  cncfcnvcn  21591  evth  21625  nmhmcn  21769  cmsss  21955  lssbn  21956  srabn  21966  ishl2  21976  ivthlem2  22030  0plef  22245  itg2monolem1  22323  itg2cnlem1  22334  itg2cnlem2  22335  ellimc2  22447  dvne0  22578  ellogdm  23188  dcubic  23374  atans2  23459  amgm  23518  ftalem3  23546  pclogsum  23688  dchrelbas3  23711  lgsabs1  23807  dchrvmaeq0  23887  rpvmasum2  23895  ajval  25975  bnsscmcl  25982  axhcompl-zf  26113  seq1hcau  26302  hlim2  26307  issh3  26335  lnopcnre  27156  dmdbr2  27420  elatcv0  27458  iunsnima  27685  1stmbfm  28468  2ndmbfm  28469  eulerpartlemd  28569  cvmlift2lem12  29023  elpredg  29498  istotbnd2  30506  sstotbnd2  30510  isbnd3b  30521  totbndbnd  30525  islnr2  31304  sdrgacs  31391  areaquad  31425  oddm1evenALTV  32581  oddp1evenALTV  32582