Theorem baib 872

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

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359

This theorem is referenced by:  baibr  873  rbaib  874  ceqsrexbv  3030  elrab3  3053  dfpss3  3393  rabsn  3833  elrint2  4052  nlimon  4790  limom  4819  fnres  5520  fvmpti  5764  f1ompt  5850  fliftfun  5993  isocnv3  6011  ovid  6149  riotaxfrd  6540  brdifun  6891  xpcomco  7157  0sdomg  7195  f1finf1o  7294  ordtypelem9  7451  isacn  7881  alephinit  7932  isfin5-2  8227  pwfseqlem1  8489  pwfseqlem3  8491  pwfseqlem4  8493  ltresr  8971  xrlenlt  9099  znnnlt1  10264  difrp  10601  elfz  11005  fzolb2  11101  elfzo3  11110  fzouzsplit  11123  caubnd  12117  ello12  12265  elo12  12276  bitsval2  12892  smueqlem  12957  rpexp  13075  ramcl  13352  ismon2  13915  isepi2  13922  isfull2  14063  isfth2  14067  isghm3  14962  gastacos  15042  sylow2alem2  15207  lssnle  15261  isabl2  15375  submcmn2  15413  iscyggen2  15446  iscyg3  15451  cyggexb  15463  gsum2d2  15503  dprdw  15523  dprd2da  15555  iscrng2  15634  dvdsr2  15707  dfrhm2  15776  islmhm3  16059  isdomn2  16314  psrbaglefi  16392  mplsubrglem  16457  prmirredlem  16728  chrnzr  16766  iunocv  16863  iscss2  16868  ishil2  16901  obselocv  16910  bastop1  17013  isclo  17106  maxlp  17165  isperf2  17170  restperf  17202  cnpnei  17282  cnntr  17293  cnprest  17307  cnprest2  17308  lmres  17318  iscnrm2  17356  ist0-2  17362  ist1-2  17365  ishaus2  17369  tgcmp  17418  cmpfi  17425  dfcon2  17435  t1conperf  17452  subislly  17497  tx1cn  17594  tx2cn  17595  xkopt  17640  xkoinjcn  17672  ist0-4  17714  trfil2  17872  fin1aufil  17917  flimtopon  17955  elflim  17956  fclstopon  17997  isfcls2  17998  alexsubALTlem4  18034  ptcmplem3  18038  tgphaus  18099  xmetec  18417  prdsbl  18474  blval2  18558  isnvc2  18687  isnghm2  18711  isnmhm2  18739  0nmhm  18742  xrtgioo  18790  cncfcnvcn  18904  evth  18937  nmhmcn  19081  cmsss  19256  lssbn  19257  srabn  19267  ishl2  19277  ivthlem2  19302  0plef  19517  itg2monolem1  19595  itg2cnlem1  19606  itg2cnlem2  19607  ellimc2  19717  dvne0  19848  ellogdm  20483  dcubic  20639  atans2  20724  amgm  20782  ftalem3  20810  pclogsum  20952  dchrelbas3  20975  lgsabs1  21071  dchrvmaeq0  21151  rpvmasum2  21159  ajval  22316  bnsscmcl  22323  axhcompl-zf  22454  seq1hcau  22642  hlim2  22647  issh3  22675  lnopcnre  23495  dmdbr2  23759  elatcv0  23797  isarchi  24205  1stmbfm  24563  2ndmbfm  24564  cvmlift2lem12  24954  elpredg  25392  dffun10  25667  istotbnd2  26369  sstotbnd2  26373  isbnd3b  26384  totbndbnd  26388  islnr2  27186  sdrgacs  27377

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361