Theorem baib 912

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  913  rbaibOLD  916  ceqsrexbv  3207  elrab3  3231  dfpss3  3552  rabsn  4065  elrint2  4296  elpredg  5411  fnres  5708  fvmpti  5961  f1ompt  6057  fliftfun  6218  isocnv3  6236  riotaxfrd  6295  ovid  6425  nlimon  6690  limom  6719  brdifun  7396  xpcomco  7666  0sdomg  7705  f1finf1o  7802  ordtypelem9  8045  isacn  8477  alephinit  8528  isfin5-2  8823  pwfseqlem1  9085  pwfseqlem3  9087  pwfseqlem4  9089  ltresr  9566  xrlenlt  9701  znnnlt1  10966  difrp  11339  elfz  11792  fzolb2  11929  elfzo3  11938  fzouzsplit  11955  rabssnn0fi  12199  caubnd  13415  ello12  13573  elo12  13584  bitsval2  14391  smueqlem  14457  rpexp  14665  ramcl  14980  ismon2  15632  isepi2  15639  isfull2  15809  isfth2  15813  isghm3  16877  gastacos  16957  sylow2alem2  17263  lssnle  17317  isabl2  17431  submcmn2  17472  iscyggen2  17509  iscyg3  17514  cyggexb  17526  gsum2d2  17599  dprdw  17635  dprd2da  17668  iscrng2  17789  dvdsr2  17868  dfrhm2  17938  islmhm3  18244  isdomn2  18516  psrbaglefi  18589  mplsubrglem  18656  prmirredlem  19056  chrnzr  19093  iunocv  19236  iscss2  19241  ishil2  19274  obselocv  19283  bastop1  20001  isclo  20095  maxlp  20155  isperf2  20160  restperf  20192  cnpnei  20272  cnntr  20283  cnprest  20297  cnprest2  20298  lmres  20308  iscnrm2  20346  ist0-2  20352  ist1-2  20355  ishaus2  20359  tgcmp  20408  cmpfi  20415  dfcon2  20426  t1conperf  20443  subislly  20488  tx1cn  20616  tx2cn  20617  xkopt  20662  xkoinjcn  20694  ist0-4  20736  trfil2  20894  fin1aufil  20939  flimtopon  20977  elflim  20978  fclstopon  21019  isfcls2  21020  alexsubALTlem4  21057  ptcmplem3  21061  tgphaus  21123  xmetec  21441  prdsbl  21498  blval2  21569  isnvc2  21693  isnghm2  21721  isnghm2OLD  21739  isnmhm2  21765  0nmhm  21768  xrtgioo  21816  cncfcnvcn  21945  evth  21979  nmhmcn  22126  cmsss  22310  lssbn  22311  srabn  22319  ishl2  22329  ivthlem2  22395  0plef  22622  itg2monolem1  22700  itg2cnlem1  22711  itg2cnlem2  22712  ellimc2  22824  dvne0  22955  ellogdm  23576  dcubic  23764  atans2  23849  amgm  23908  ftalem3  23991  pclogsum  24135  dchrelbas3  24158  lgsabs1  24254  dchrvmaeq0  24334  rpvmasum2  24342  ajval  26495  bnsscmcl  26502  axhcompl-zf  26643  seq1hcau  26832  hlim2  26837  issh3  26864  lnopcnre  27684  dmdbr2  27948  elatcv0  27986  iunsnima  28220  1stmbfm  29084  2ndmbfm  29085  eulerpartlemd  29201  cvmlift2lem12  30039  topdifinfeq  31700  istotbnd2  32022  sstotbnd2  32026  isbnd3b  32037  totbndbnd  32041  islnr2  35899  sdrgacs  35993  areaquad  36027  oddm1evenALTV  38522  oddp1evenALTV  38523