Theorem baib 891

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 501	. 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  892  rbaib  893  ceqsrexbv  3091  elrab3  3115  dfpss3  3439  rabsn  3939  elrint2  4167  fnres  5524  fvmpti  5770  f1ompt  5862  fliftfun  6002  isocnv3  6020  riotaxfrd  6081  ovid  6206  nlimon  6461  limom  6490  brdifun  7124  xpcomco  7397  0sdomg  7436  f1finf1o  7535  ordtypelem9  7736  isacn  8210  alephinit  8261  isfin5-2  8556  pwfseqlem1  8821  pwfseqlem3  8823  pwfseqlem4  8825  ltresr  9303  xrlenlt  9438  znnnlt1  10669  difrp  11020  elfz  11439  fzolb2  11555  elfzo3  11564  fzouzsplit  11580  caubnd  12842  ello12  12990  elo12  13001  bitsval2  13617  smueqlem  13682  rpexp  13802  ramcl  14086  ismon2  14669  isepi2  14676  isfull2  14817  isfth2  14821  isghm3  15741  gastacos  15821  sylow2alem2  16110  lssnle  16164  isabl2  16278  submcmn2  16316  iscyggen2  16351  iscyg3  16356  cyggexb  16368  gsum2d2  16456  dprdw  16484  dprdwOLD  16490  dprd2da  16531  iscrng2  16650  dvdsr2  16729  dfrhm2  16798  islmhm3  17087  isdomn2  17349  psrbaglefi  17431  psrbaglefiOLD  17432  mplsubrglem  17507  mplsubrglemOLD  17508  prmirredlem  17817  prmirredlemOLD  17820  chrnzr  17861  iunocv  18006  iscss2  18011  ishil2  18044  obselocv  18053  bastop1  18498  isclo  18591  maxlp  18651  isperf2  18656  restperf  18688  cnpnei  18768  cnntr  18779  cnprest  18793  cnprest2  18794  lmres  18804  iscnrm2  18842  ist0-2  18848  ist1-2  18851  ishaus2  18855  tgcmp  18904  cmpfi  18911  dfcon2  18923  t1conperf  18940  subislly  18985  tx1cn  19082  tx2cn  19083  xkopt  19128  xkoinjcn  19160  ist0-4  19202  trfil2  19360  fin1aufil  19405  flimtopon  19443  elflim  19444  fclstopon  19485  isfcls2  19486  alexsubALTlem4  19522  ptcmplem3  19526  tgphaus  19587  xmetec  19909  prdsbl  19966  blval2  20050  isnvc2  20179  isnghm2  20203  isnmhm2  20231  0nmhm  20234  xrtgioo  20283  cncfcnvcn  20397  evth  20431  nmhmcn  20575  cmsss  20761  lssbn  20762  srabn  20772  ishl2  20782  ivthlem2  20836  0plef  21050  itg2monolem1  21128  itg2cnlem1  21139  itg2cnlem2  21140  ellimc2  21252  dvne0  21383  ellogdm  22027  dcubic  22184  atans2  22269  amgm  22327  ftalem3  22355  pclogsum  22497  dchrelbas3  22520  lgsabs1  22616  dchrvmaeq0  22696  rpvmasum2  22704  ebtwntg  23147  ajval  24181  bnsscmcl  24188  axhcompl-zf  24319  seq1hcau  24508  hlim2  24513  issh3  24541  lnopcnre  25362  dmdbr2  25626  elatcv0  25664  isarchi  26116  1stmbfm  26595  2ndmbfm  26596  eulerpartlemd  26663  cvmlift2lem12  27117  elpredg  27552  istotbnd2  28578  sstotbnd2  28582  isbnd3b  28593  totbndbnd  28597  islnr2  29379  sdrgacs  29467  areaquad  29501