Theorem biimpi 119

Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
biimpi.1	|- ( ph <-> ps )

Assertion

Ref	Expression
biimpi	|- ( ph -> ps )

Proof of Theorem biimpi

Step	Hyp	Ref	Expression
1		biimpi.1	. 2 |- ( ph <-> ps )
2		bi1 117	. 2 |- ( ( ph <-> ps ) -> ( ph -> ps ) )
3	1, 2	ax-mp 5	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbi  120  sylib  121  sylbb  122  biimpri  132  mpbi  144  syl5bi  151  syl6ib  160  syl7bi  164  syl8ib  165  bitri  183  simplbi  272  simprbi  273  sylanb  282  sylan2b  285  anc2l  325  sylanblc  411  orbi2i  751  pm2.32  758  oranim  770  stabnot  818  exmiddc  821  pm2.1dc  822  stdcndcOLD  831  stdcn  832  imanst  873  pm5.75  946  rnlem  960  simp1bi  996  simp2bi  997  simp3bi  998  syl3an1b  1252  syl3an2b  1253  syl3an3b  1254  exalim  1478  nford  1546  stdpc5  1563  sbbii  1738  sb9i  1953  eu5  2044  exmoeudc  2060  eqeq1  2144  eleq2  2201  nner  2310  rexalim  2428  gencbvex  2727  gencbval  2729  moeq  2854  euind  2866  reuind  2884  ssel  3086  ssrmof  3155  unssd  3247  ssind  3295  unssdif  3306  ss0  3398  prprc  3628  disjnim  3915  trint  4036  snexprc  4105  undifexmid  4112  exmidn0m  4119  exmidsssn  4120  exmidundif  4124  exmidundifim  4125  pocl  4220  sotritrieq  4242  frirrg  4267  unexg  4359  abnex  4363  reusv3i  4375  ordtriexmid  4432  ordtri2orexmid  4433  preleq  4465  0elsucexmid  4475  ordpwsucexmid  4480  ordtri2or2exmid  4481  elnn  4514  brrelex12  4572  0nelrel  4580  elrel  4636  xpssres  4849  elres  4850  coi2  5050  iotabi  5092  uniabio  5093  nfunv  5151  funun  5162  funcnv3  5180  funimass1  5195  imain  5200  funssxp  5287  f0dom0  5311  f1o00  5395  fsn2  5587  isoselem  5714  oprabid  5796  brabvv  5810  oprssdmm  6062  1stdm  6073  f1o2ndf1  6118  poxp  6122  rdgon  6276  frecfcllem  6294  nntri3or  6382  nntri1  6385  ensym  6668  xpen  6732  snnen2oprc  6747  phplem4on  6754  fict  6755  fidceq  6756  infiexmid  6764  php5fin  6769  fisbth  6770  fin0  6772  fin0or  6773  diffisn  6780  infnfi  6782  en2eqpr  6794  exmidpw  6795  fientri3  6796  unsnfi  6800  unsnfidcex  6801  unsnfidcel  6802  undifdcss  6804  ssfidc  6816  relcnvfi  6822  fiuni  6859  eqinfti  6900  djulclb  6933  updjud  6960  omp1eomlem  6972  0ct  6985  ctmlemr  6986  ctssdclemn0  6988  ctssdccl  6989  enomnilem  7003  finomni  7005  exmidomni  7007  enq0sym  7233  enq0tr  7235  prarloclem3  7298  nqprl  7352  nqpru  7353  addnqprlemrl  7358  addnqprlemru  7359  addnqprlemfl  7360  addnqprlemfu  7361  mulnqprlemrl  7374  mulnqprlemru  7375  mulnqprlemfl  7376  mulnqprlemfu  7377  ltexprlemfl  7410  ltexprlemfu  7412  recexprlemopl  7426  recexprlemopu  7428  aptipr  7442  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  caucvgprlemladdfu  7478  caucvgprprlemexbt  7507  suplocexprlemrl  7518  suplocexprlemru  7520  suplocexprlemex  7523  srpospr  7584  elrealeu  7630  axarch  7692  axcaucvglemres  7700  nn0ge2m1nn  9030  elnn0z  9060  peano2z  9083  uzm1  9349  qapne  9424  rpregt0  9448  rpnegap  9467  npnflt  9591  nmnfgt  9594  xaddf  9620  xaddval  9621  xltadd1  9652  xsubge0  9657  xleaddadd  9663  elfz1end  9828  1fv  9909  elfzonlteqm1  9980  qtri3or  10013  exbtwnzlemshrink  10019  rebtwn2zlemshrink  10024  ioom  10031  modfzo0difsn  10161  modsumfzodifsn  10162  addmodlteq  10164  frecfzennn  10192  seq3f1olemstep  10267  ser0  10280  exp3vallem  10287  facp1  10469  faclbnd  10480  bcn1  10497  hashennnuni  10518  hashcl  10520  hashfz1  10522  hashen  10523  fihashdom  10542  hashun  10544  zfz1isolem1  10576  zfz1iso  10577  sqrt0  10769  resqrexlemfp1  10774  cau3lem  10879  xrmaxifle  11008  xrmaxiflemval  11012  xrmaxltsup  11020  xrmaxadd  11023  climserle  11107  climcaucn  11113  iserabs  11237  isumshft  11252  cvgratgt0  11295  mertenslem2  11298  prodf1  11304  eirrap  11473  bezoutlemzz  11679  dfgcd3  11687  lcmcllem  11737  prmind2  11790  prm2orodd  11796  sqrt2irr0  11831  sqrt2irrap  11847  ennnfonelemjn  11904  ennnfonelemdm  11922  ennnfonelemim  11926  ctiunctlemfo  11941  isstructr  11963  isbasis3g  12202  innei  12321  cnpnei  12377  cncnp2m  12389  cnptopresti  12396  cnptoprest2  12398  imasnopn  12457  xmettx  12668  cdivcncfap  12745  expcncf  12750  cnopnap  12752  ivthinclemdisj  12776  dvrecap  12835  ex-ceil  12927  bj-nnbist  12942  bj-sucexg  13109  bj-om  13124  bj-inf2vnlem1  13157  exmid1stab  13184  trilpolemisumle  13220