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  763  pm2.32  770  oranim  782  stabnot  834  exmiddc  837  pm2.1dc  838  stdcndcOLD  847  stdcn  848  const  853  imanst  889  pm5.75  964  rnlem  978  simp1bi  1014  simp2bi  1015  simp3bi  1016  syl3an1b  1285  syl3an2b  1286  syl3an3b  1287  exalim  1516  nford  1581  nfal  1590  stdpc5  1598  sbbii  1779  sb9i  1999  eu5  2092  exmoeudc  2108  eqeq1  2203  eleq2  2260  nner  2371  rexalim  2490  gencbvex  2810  gencbval  2812  moeq  2939  euind  2951  reuind  2969  ssel  3178  ssrmof  3247  unssd  3340  ssind  3388  unssdif  3399  ss0  3492  prprc  3733  disjnim  4025  trint  4147  snexprc  4220  undifexmid  4227  exmidn0m  4235  exmidsssn  4236  exmidundif  4240  exmidundifim  4241  exmid1stab  4242  pocl  4339  sotritrieq  4361  frirrg  4386  unexg  4479  abnex  4483  reusv3i  4495  ordtriexmid  4558  ontriexmidim  4559  ordtri2orexmid  4560  preleq  4592  0elsucexmid  4602  ordpwsucexmid  4607  ordtri2or2exmid  4608  elomssom  4642  brrelex12  4702  0nelrel  4710  elrel  4766  xpssres  4982  elres  4983  coi2  5187  iotabi  5229  uniabio  5230  nfunv  5292  funun  5303  funcnv3  5321  funimass1  5336  imain  5341  funssxp  5430  f0dom0  5454  f1o00  5542  fsn2  5739  isoselem  5870  oprabid  5957  brabvv  5972  uchoice  6204  oprssdmm  6238  1stdm  6249  f1o2ndf1  6295  poxp  6299  rdgon  6453  frecfcllem  6471  nntri3or  6560  nntri1  6563  ensym  6849  xpen  6915  snnen2oprc  6930  phplem4on  6937  fict  6938  fidceq  6939  infiexmid  6947  php5fin  6952  fisbth  6953  fin0  6955  fin0or  6956  diffisn  6963  infnfi  6965  en2eqpr  6977  exmidpw  6978  exmidpweq  6979  pw1fin  6980  fientri3  6985  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  undifdcss  6993  ssfidc  7007  relcnvfi  7016  fiuni  7053  eqinfti  7095  djulclb  7130  updjud  7157  omp1eomlem  7169  0ct  7182  ctmlemr  7183  ctssdclemn0  7185  ctssdccl  7186  enomnilem  7213  finomni  7215  exmidomni  7217  enmkvlem  7236  enwomnilem  7244  exmidontriimlem1  7304  onntri35  7320  onntri52  7327  dftap2  7334  exmidapne  7343  enq0sym  7516  enq0tr  7518  prarloclem3  7581  nqprl  7635  nqpru  7636  addnqprlemrl  7641  addnqprlemru  7642  addnqprlemfl  7643  addnqprlemfu  7644  mulnqprlemrl  7657  mulnqprlemru  7658  mulnqprlemfl  7659  mulnqprlemfu  7660  ltexprlemfl  7693  ltexprlemfu  7695  recexprlemopl  7709  recexprlemopu  7711  aptipr  7725  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  caucvgprlemladdfu  7761  caucvgprprlemexbt  7790  suplocexprlemrl  7801  suplocexprlemru  7803  suplocexprlemex  7806  srpospr  7867  elrealeu  7913  axarch  7975  axcaucvglemres  7983  nn0ge2m1nn  9326  elnn0z  9356  peano2z  9379  uzm1  9649  qapne  9730  rpregt0  9759  rpnegap  9778  xnn0dcle  9894  xnn0letri  9895  npnflt  9907  nmnfgt  9910  xaddf  9936  xaddval  9937  xltadd1  9968  xsubge0  9973  xleaddadd  9979  elfz1end  10147  1fv  10231  elfzonlteqm1  10303  qtri3or  10347  exbtwnzlemshrink  10355  rebtwn2zlemshrink  10360  ioom  10367  elicore  10373  modfzo0difsn  10504  modsumfzodifsn  10505  addmodlteq  10507  frecfzennn  10535  seq3f1olemstep  10623  ser0  10642  exp3vallem  10649  facp1  10839  faclbnd  10850  bcn1  10867  hashennnuni  10888  hashcl  10890  hashfz1  10892  hashen  10893  fihashdom  10912  hashun  10914  zfz1isolem1  10949  zfz1iso  10950  lencl  10956  sswrd  10961  sqrt0  11186  resqrexlemfp1  11191  cau3lem  11296  xrmaxifle  11428  xrmaxiflemval  11432  xrmaxltsup  11440  xrmaxadd  11443  climserle  11527  climcaucn  11533  iserabs  11657  isumshft  11672  cvgratgt0  11715  mertenslem2  11718  prodf1  11724  fprodunsn  11786  fprodfac  11797  eirrap  11960  bezoutlemzz  12194  dfgcd3  12202  nnmindc  12226  nnminle  12227  nninfctlemfo  12232  lcmcllem  12260  prmind2  12313  prm2orodd  12319  sqrt2irr0  12357  sqrt2irrap  12373  ennnfonelemjn  12644  ennnfonelemdm  12662  ennnfonelemim  12666  ctiunctlemfo  12681  isstructr  12718  basmex  12762  dfgrp2  13229  dfgrp3mlem  13300  mulgnngsum  13333  grpissubg  13400  ablsubsub23  13531  rrgmex  13893  lssmex  13987  lidlmex  14107  2idlmex  14133  df2idl2  14141  2idlss  14146  isbasis3g  14366  innei  14483  cnpnei  14539  cncnp2m  14551  cnptopresti  14558  cnptoprest2  14560  imasnopn  14619  xmettx  14830  cdivcncfap  14924  expcncf  14929  cnopnap  14931  ivthinclemdisj  14960  dvrecap  15033  dvmptfsum  15045  gausslemma2dlem0i  15382  gausslemma2dlem1a  15383  2lgslem1c  15415  2sqlem10  15450  ex-ceil  15456  bj-nnbist  15474  bj-con1st  15481  bj-charfunbi  15541  bj-sucexg  15652  bj-om  15667  bj-inf2vnlem1  15700  trilpolemisumle  15769  cndcap  15790