Theorem baib 896

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  897  rbaib  898  ceqsrexbv  3094  elrab3  3118  dfpss3  3442  rabsn  3942  elrint2  4170  fnres  5527  fvmpti  5773  f1ompt  5865  fliftfun  6005  isocnv3  6023  riotaxfrd  6083  ovid  6207  nlimon  6462  limom  6491  brdifun  7128  xpcomco  7401  0sdomg  7440  f1finf1o  7539  ordtypelem9  7740  isacn  8214  alephinit  8265  isfin5-2  8560  pwfseqlem1  8825  pwfseqlem3  8827  pwfseqlem4  8829  ltresr  9307  xrlenlt  9442  znnnlt1  10673  difrp  11024  elfz  11443  fzolb2  11559  elfzo3  11568  fzouzsplit  11584  caubnd  12846  ello12  12994  elo12  13005  bitsval2  13621  smueqlem  13686  rpexp  13806  ramcl  14090  ismon2  14673  isepi2  14680  isfull2  14821  isfth2  14825  isghm3  15748  gastacos  15828  sylow2alem2  16117  lssnle  16171  isabl2  16285  submcmn2  16323  iscyggen2  16358  iscyg3  16363  cyggexb  16375  gsum2d2  16466  dprdw  16494  dprdwOLD  16500  dprd2da  16541  iscrng2  16660  dvdsr2  16739  dfrhm2  16808  islmhm3  17109  isdomn2  17371  psrbaglefi  17441  psrbaglefiOLD  17442  mplsubrglem  17517  mplsubrglemOLD  17518  prmirredlem  17917  prmirredlemOLD  17920  chrnzr  17961  iunocv  18106  iscss2  18111  ishil2  18144  obselocv  18153  bastop1  18598  isclo  18691  maxlp  18751  isperf2  18756  restperf  18788  cnpnei  18868  cnntr  18879  cnprest  18893  cnprest2  18894  lmres  18904  iscnrm2  18942  ist0-2  18948  ist1-2  18951  ishaus2  18955  tgcmp  19004  cmpfi  19011  dfcon2  19023  t1conperf  19040  subislly  19085  tx1cn  19182  tx2cn  19183  xkopt  19228  xkoinjcn  19260  ist0-4  19302  trfil2  19460  fin1aufil  19505  flimtopon  19543  elflim  19544  fclstopon  19585  isfcls2  19586  alexsubALTlem4  19622  ptcmplem3  19626  tgphaus  19687  xmetec  20009  prdsbl  20066  blval2  20150  isnvc2  20279  isnghm2  20303  isnmhm2  20331  0nmhm  20334  xrtgioo  20383  cncfcnvcn  20497  evth  20531  nmhmcn  20675  cmsss  20861  lssbn  20862  srabn  20872  ishl2  20882  ivthlem2  20936  0plef  21150  itg2monolem1  21228  itg2cnlem1  21239  itg2cnlem2  21240  ellimc2  21352  dvne0  21483  ellogdm  22084  dcubic  22241  atans2  22326  amgm  22384  ftalem3  22412  pclogsum  22554  dchrelbas3  22577  lgsabs1  22673  dchrvmaeq0  22753  rpvmasum2  22761  ebtwntg  23228  ajval  24262  bnsscmcl  24269  axhcompl-zf  24400  seq1hcau  24589  hlim2  24594  issh3  24622  lnopcnre  25443  dmdbr2  25707  elatcv0  25745  isarchi  26199  1stmbfm  26675  2ndmbfm  26676  eulerpartlemd  26749  cvmlift2lem12  27203  elpredg  27639  istotbnd2  28669  sstotbnd2  28673  isbnd3b  28684  totbndbnd  28688  islnr2  29470  sdrgacs  29558  areaquad  29592  rabssnn0fi  30747