Theorem biimpi 120

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		biimp 118	. 2 |- ( ( ph <-> ps ) -> ( ph -> ps ) )
3	1, 2	ax-mp 5	1 |- ( ph -> ps )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbi  121  sylib  122  sylbb  123  biimpri  133  mpbi  145  biimtrid  152  imbitrdi  161  syl7bi  165  syl8ib  166  bitri  184  simplbi  274  simprbi  275  sylanb  284  sylan2b  287  anc2l  327  sylanblc  415  orbi2i  769  pm2.32  776  oranim  788  stabnot  840  exmiddc  843  pm2.1dc  844  stdcndcOLD  853  stdcn  854  const  859  imanst  895  pm5.75  970  rnlem  984  ifpnst  996  simp1bi  1038  simp2bi  1039  simp3bi  1040  syl3an1b  1309  syl3an2b  1310  syl3an3b  1311  exalim  1550  nford  1615  nfal  1624  stdpc5  1632  sbbii  1813  sb9i  2033  eu5  2127  exmoeudc  2143  eqeq1  2238  eleq2  2295  nner  2406  rexalim  2525  gencbvex  2850  gencbval  2852  moeq  2981  euind  2993  reuind  3011  ssel  3221  ssrmof  3290  unssd  3383  ssind  3431  unssdif  3442  ss0  3535  rabsnif  3738  prprc  3782  disjnim  4078  trint  4202  snexprc  4276  undifexmid  4283  exmidn0m  4291  exmidsssn  4292  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  pocl  4400  sotritrieq  4422  frirrg  4447  unexg  4540  abnex  4544  reusv3i  4556  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  preleq  4653  0elsucexmid  4663  ordpwsucexmid  4668  ordtri2or2exmid  4669  elomssom  4703  brrelex12  4764  0nelrel  4772  elrel  4828  xpssres  5048  elres  5049  coi2  5253  iotabi  5296  uniabio  5297  nfunv  5359  funun  5371  funcnv3  5392  funimass1  5407  imain  5412  funssxp  5504  f0dom0  5531  f1o00  5621  fsn2  5822  funopsn  5831  isoselem  5964  oprabid  6053  brabvv  6070  uchoice  6303  oprssdmm  6337  1stdm  6348  f1o2ndf1  6396  poxp  6400  rdgon  6555  frecfcllem  6573  nntri3or  6664  nntri1  6667  ensym  6958  en2  7001  xpen  7034  snnen2oprc  7049  phplem4on  7057  fict  7058  fidceq  7059  infiexmid  7069  php5fin  7074  fisbth  7075  fin0  7077  fin0or  7078  diffisn  7085  infnfi  7087  fidcen  7091  en2eqpr  7102  exmidpw  7103  exmidpweq  7104  pw1fin  7105  fientri3  7110  unsnfi  7114  unsnfidcex  7115  unsnfidcel  7116  undifdcss  7118  ssfidc  7133  relcnvfi  7143  fiuni  7180  eqinfti  7222  djulclb  7257  updjud  7284  omp1eomlem  7296  0ct  7309  ctmlemr  7310  ctssdclemn0  7312  ctssdccl  7313  enomnilem  7340  finomni  7342  exmidomni  7344  enmkvlem  7363  enwomnilem  7371  exmidontriimlem1  7439  onntri35  7458  onntri52  7465  dftap2  7473  exmidapne  7482  enq0sym  7655  enq0tr  7657  prarloclem3  7720  nqprl  7774  nqpru  7775  addnqprlemrl  7780  addnqprlemru  7781  addnqprlemfl  7782  addnqprlemfu  7783  mulnqprlemrl  7796  mulnqprlemru  7797  mulnqprlemfl  7798  mulnqprlemfu  7799  ltexprlemfl  7832  ltexprlemfu  7834  recexprlemopl  7848  recexprlemopu  7850  aptipr  7864  cauappcvgprlemladdfu  7877  cauappcvgprlemladdfl  7878  caucvgprlemladdfu  7900  caucvgprprlemexbt  7929  suplocexprlemrl  7940  suplocexprlemru  7942  suplocexprlemex  7945  srpospr  8006  elrealeu  8052  axarch  8114  axcaucvglemres  8122  nn0ge2m1nn  9465  elnn0z  9495  peano2z  9518  uzm1  9790  qapne  9876  rpregt0  9905  rpnegap  9924  xnn0dcle  10040  xnn0letri  10041  npnflt  10053  nmnfgt  10056  xaddf  10082  xaddval  10083  xltadd1  10114  xsubge0  10119  xleaddadd  10125  elfz1end  10293  1fv  10377  elfzonlteqm1  10459  qtri3or  10504  exbtwnzlemshrink  10512  rebtwn2zlemshrink  10517  ioom  10524  elicore  10530  modfzo0difsn  10661  modsumfzodifsn  10662  addmodlteq  10664  frecfzennn  10692  seq3f1olemstep  10780  ser0  10799  exp3vallem  10806  facp1  10996  faclbnd  11007  bcn1  11024  hashennnuni  11045  hashcl  11047  hashfz1  11049  hashen  11050  fihashdom  11070  hashun  11072  zfz1isolem1  11108  zfz1iso  11109  lencl  11124  sswrd  11129  swrdswrd  11293  swrdccatin2  11317  pfxccat3  11322  pfxccatpfx1  11324  sqrt0  11585  resqrexlemfp1  11590  cau3lem  11695  xrmaxifle  11827  xrmaxiflemval  11831  xrmaxltsup  11839  xrmaxadd  11842  climserle  11926  climcaucn  11932  iserabs  12057  isumshft  12072  cvgratgt0  12115  mertenslem2  12118  prodf1  12124  fprodunsn  12186  fprodfac  12197  eirrap  12360  bezoutlemzz  12594  dfgcd3  12602  nnmindc  12626  nnminle  12627  nninfctlemfo  12632  lcmcllem  12660  prmind2  12713  prm2orodd  12719  sqrt2irr0  12757  sqrt2irrap  12773  ennnfonelemjn  13044  ennnfonelemdm  13062  ennnfonelemim  13066  ctiunctlemfo  13081  isstructr  13118  basmex  13163  dfgrp2  13631  dfgrp3mlem  13702  mulgnngsum  13735  grpissubg  13802  ablsubsub23  13933  rrgmex  14297  lssmex  14391  lidlmex  14511  2idlmex  14537  df2idl2  14545  2idlss  14550  isbasis3g  14797  innei  14914  cnpnei  14970  cncnp2m  14982  cnptopresti  14989  cnptoprest2  14991  imasnopn  15050  xmettx  15261  cdivcncfap  15355  expcncf  15360  cnopnap  15362  ivthinclemdisj  15391  dvrecap  15464  dvmptfsum  15476  gausslemma2dlem0i  15813  gausslemma2dlem1a  15814  2lgslem1c  15846  2sqlem10  15881  lfgredg2dom  16010  ausgrusgrben  16046  ausgrumgrien  16048  ausgrusgrien  16049  uspgredg2vlem  16098  uspgredg2v  16099  usgredg2vlem2  16101  ushgredgedg  16104  ushgredgedgloop  16106  griedg0ssusgr  16129  vtxedgfi  16167  vtxlpfi  16168  wlk1walkdom  16237  wlk0prc  16250  clwwlknonex2  16317  eupthi  16327  ex-ceil  16377  bj-nnbist  16399  bj-con1st  16406  bj-charfunbi  16465  bj-sucexg  16576  bj-om  16591  bj-inf2vnlem1  16624  trilpolemisumle  16701  cndcap  16723  gfsumval  16740