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  767  pm2.32  774  oranim  786  stabnot  838  exmiddc  841  pm2.1dc  842  stdcndcOLD  851  stdcn  852  const  857  imanst  893  pm5.75  968  rnlem  982  ifpnst  994  simp1bi  1036  simp2bi  1037  simp3bi  1038  syl3an1b  1307  syl3an2b  1308  syl3an3b  1309  exalim  1548  nford  1613  nfal  1622  stdpc5  1630  sbbii  1811  sb9i  2031  eu5  2125  exmoeudc  2141  eqeq1  2236  eleq2  2293  nner  2404  rexalim  2523  gencbvex  2847  gencbval  2849  moeq  2978  euind  2990  reuind  3008  ssel  3218  ssrmof  3287  unssd  3380  ssind  3428  unssdif  3439  ss0  3532  prprc  3777  disjnim  4073  trint  4197  snexprc  4271  undifexmid  4278  exmidn0m  4286  exmidsssn  4287  exmidundif  4291  exmidundifim  4292  exmid1stab  4293  pocl  4395  sotritrieq  4417  frirrg  4442  unexg  4535  abnex  4539  reusv3i  4551  ordtriexmid  4614  ontriexmidim  4615  ordtri2orexmid  4616  preleq  4648  0elsucexmid  4658  ordpwsucexmid  4663  ordtri2or2exmid  4664  elomssom  4698  brrelex12  4759  0nelrel  4767  elrel  4823  xpssres  5043  elres  5044  coi2  5248  iotabi  5291  uniabio  5292  nfunv  5354  funun  5365  funcnv3  5386  funimass1  5401  imain  5406  funssxp  5498  f0dom0  5524  f1o00  5613  fsn2  5814  funopsn  5822  isoselem  5953  oprabid  6042  brabvv  6059  uchoice  6292  oprssdmm  6326  1stdm  6337  f1o2ndf1  6385  poxp  6389  rdgon  6543  frecfcllem  6561  nntri3or  6652  nntri1  6655  ensym  6946  en2  6986  xpen  7019  snnen2oprc  7034  phplem4on  7042  fict  7043  fidceq  7044  infiexmid  7052  php5fin  7057  fisbth  7058  fin0  7060  fin0or  7061  diffisn  7068  infnfi  7070  fidcen  7074  en2eqpr  7085  exmidpw  7086  exmidpweq  7087  pw1fin  7088  fientri3  7093  unsnfi  7097  unsnfidcex  7098  unsnfidcel  7099  undifdcss  7101  ssfidc  7115  relcnvfi  7124  fiuni  7161  eqinfti  7203  djulclb  7238  updjud  7265  omp1eomlem  7277  0ct  7290  ctmlemr  7291  ctssdclemn0  7293  ctssdccl  7294  enomnilem  7321  finomni  7323  exmidomni  7325  enmkvlem  7344  enwomnilem  7352  exmidontriimlem1  7419  onntri35  7438  onntri52  7445  dftap2  7453  exmidapne  7462  enq0sym  7635  enq0tr  7637  prarloclem3  7700  nqprl  7754  nqpru  7755  addnqprlemrl  7760  addnqprlemru  7761  addnqprlemfl  7762  addnqprlemfu  7763  mulnqprlemrl  7776  mulnqprlemru  7777  mulnqprlemfl  7778  mulnqprlemfu  7779  ltexprlemfl  7812  ltexprlemfu  7814  recexprlemopl  7828  recexprlemopu  7830  aptipr  7844  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  caucvgprlemladdfu  7880  caucvgprprlemexbt  7909  suplocexprlemrl  7920  suplocexprlemru  7922  suplocexprlemex  7925  srpospr  7986  elrealeu  8032  axarch  8094  axcaucvglemres  8102  nn0ge2m1nn  9445  elnn0z  9475  peano2z  9498  uzm1  9770  qapne  9851  rpregt0  9880  rpnegap  9899  xnn0dcle  10015  xnn0letri  10016  npnflt  10028  nmnfgt  10031  xaddf  10057  xaddval  10058  xltadd1  10089  xsubge0  10094  xleaddadd  10100  elfz1end  10268  1fv  10352  elfzonlteqm1  10433  qtri3or  10477  exbtwnzlemshrink  10485  rebtwn2zlemshrink  10490  ioom  10497  elicore  10503  modfzo0difsn  10634  modsumfzodifsn  10635  addmodlteq  10637  frecfzennn  10665  seq3f1olemstep  10753  ser0  10772  exp3vallem  10779  facp1  10969  faclbnd  10980  bcn1  10997  hashennnuni  11018  hashcl  11020  hashfz1  11022  hashen  11023  fihashdom  11042  hashun  11044  zfz1isolem1  11080  zfz1iso  11081  lencl  11093  sswrd  11098  swrdswrd  11258  swrdccatin2  11282  pfxccat3  11287  pfxccatpfx1  11289  sqrt0  11536  resqrexlemfp1  11541  cau3lem  11646  xrmaxifle  11778  xrmaxiflemval  11782  xrmaxltsup  11790  xrmaxadd  11793  climserle  11877  climcaucn  11883  iserabs  12007  isumshft  12022  cvgratgt0  12065  mertenslem2  12068  prodf1  12074  fprodunsn  12136  fprodfac  12147  eirrap  12310  bezoutlemzz  12544  dfgcd3  12552  nnmindc  12576  nnminle  12577  nninfctlemfo  12582  lcmcllem  12610  prmind2  12663  prm2orodd  12669  sqrt2irr0  12707  sqrt2irrap  12723  ennnfonelemjn  12994  ennnfonelemdm  13012  ennnfonelemim  13016  ctiunctlemfo  13031  isstructr  13068  basmex  13113  dfgrp2  13581  dfgrp3mlem  13652  mulgnngsum  13685  grpissubg  13752  ablsubsub23  13883  rrgmex  14246  lssmex  14340  lidlmex  14460  2idlmex  14486  df2idl2  14494  2idlss  14499  isbasis3g  14741  innei  14858  cnpnei  14914  cncnp2m  14926  cnptopresti  14933  cnptoprest2  14935  imasnopn  14994  xmettx  15205  cdivcncfap  15299  expcncf  15304  cnopnap  15306  ivthinclemdisj  15335  dvrecap  15408  dvmptfsum  15420  gausslemma2dlem0i  15757  gausslemma2dlem1a  15758  2lgslem1c  15790  2sqlem10  15825  lfgredg2dom  15951  ausgrusgrben  15987  ausgrumgrien  15989  ausgrusgrien  15990  uspgredg2vlem  16039  uspgredg2v  16040  usgredg2vlem2  16042  ushgredgedg  16045  ushgredgedgloop  16047  griedg0ssusgr  16070  vtxedgfi  16075  vtxlpfi  16076  wlk1walkdom  16131  wlk0prc  16144  ex-ceil  16199  bj-nnbist  16217  bj-con1st  16224  bj-charfunbi  16283  bj-sucexg  16394  bj-om  16409  bj-inf2vnlem1  16442  trilpolemisumle  16520  cndcap  16541