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  762  pm2.32  769  oranim  781  stabnot  833  exmiddc  836  pm2.1dc  837  stdcndcOLD  846  stdcn  847  const  852  imanst  888  pm5.75  962  rnlem  976  simp1bi  1012  simp2bi  1013  simp3bi  1014  syl3an1b  1274  syl3an2b  1275  syl3an3b  1276  exalim  1502  nford  1567  nfal  1576  stdpc5  1584  sbbii  1765  sb9i  1980  eu5  2073  exmoeudc  2089  eqeq1  2184  eleq2  2241  nner  2351  rexalim  2470  gencbvex  2785  gencbval  2787  moeq  2914  euind  2926  reuind  2944  ssel  3151  ssrmof  3220  unssd  3313  ssind  3361  unssdif  3372  ss0  3465  prprc  3704  disjnim  3996  trint  4118  snexprc  4188  undifexmid  4195  exmidn0m  4203  exmidsssn  4204  exmidundif  4208  exmidundifim  4209  exmid1stab  4210  pocl  4305  sotritrieq  4327  frirrg  4352  unexg  4445  abnex  4449  reusv3i  4461  ordtriexmid  4522  ontriexmidim  4523  ordtri2orexmid  4524  preleq  4556  0elsucexmid  4566  ordpwsucexmid  4571  ordtri2or2exmid  4572  elomssom  4606  brrelex12  4666  0nelrel  4674  elrel  4730  xpssres  4944  elres  4945  coi2  5147  iotabi  5189  uniabio  5190  nfunv  5251  funun  5262  funcnv3  5280  funimass1  5295  imain  5300  funssxp  5387  f0dom0  5411  f1o00  5498  fsn2  5693  isoselem  5824  oprabid  5910  brabvv  5924  oprssdmm  6175  1stdm  6186  f1o2ndf1  6232  poxp  6236  rdgon  6390  frecfcllem  6408  nntri3or  6497  nntri1  6500  ensym  6784  xpen  6848  snnen2oprc  6863  phplem4on  6870  fict  6871  fidceq  6872  infiexmid  6880  php5fin  6885  fisbth  6886  fin0  6888  fin0or  6889  diffisn  6896  infnfi  6898  en2eqpr  6910  exmidpw  6911  exmidpweq  6912  pw1fin  6913  fientri3  6917  unsnfi  6921  unsnfidcex  6922  unsnfidcel  6923  undifdcss  6925  ssfidc  6937  relcnvfi  6943  fiuni  6980  eqinfti  7022  djulclb  7057  updjud  7084  omp1eomlem  7096  0ct  7109  ctmlemr  7110  ctssdclemn0  7112  ctssdccl  7113  enomnilem  7139  finomni  7141  exmidomni  7143  enmkvlem  7162  enwomnilem  7170  exmidontriimlem1  7223  onntri35  7239  onntri52  7246  dftap2  7253  exmidapne  7262  enq0sym  7434  enq0tr  7436  prarloclem3  7499  nqprl  7553  nqpru  7554  addnqprlemrl  7559  addnqprlemru  7560  addnqprlemfl  7561  addnqprlemfu  7562  mulnqprlemrl  7575  mulnqprlemru  7576  mulnqprlemfl  7577  mulnqprlemfu  7578  ltexprlemfl  7611  ltexprlemfu  7613  recexprlemopl  7627  recexprlemopu  7629  aptipr  7643  cauappcvgprlemladdfu  7656  cauappcvgprlemladdfl  7657  caucvgprlemladdfu  7679  caucvgprprlemexbt  7708  suplocexprlemrl  7719  suplocexprlemru  7721  suplocexprlemex  7724  srpospr  7785  elrealeu  7831  axarch  7893  axcaucvglemres  7901  nn0ge2m1nn  9239  elnn0z  9269  peano2z  9292  uzm1  9561  qapne  9642  rpregt0  9670  rpnegap  9689  xnn0dcle  9805  xnn0letri  9806  npnflt  9818  nmnfgt  9821  xaddf  9847  xaddval  9848  xltadd1  9879  xsubge0  9884  xleaddadd  9890  elfz1end  10058  1fv  10142  elfzonlteqm1  10213  qtri3or  10246  exbtwnzlemshrink  10252  rebtwn2zlemshrink  10257  ioom  10264  elicore  10270  modfzo0difsn  10398  modsumfzodifsn  10399  addmodlteq  10401  frecfzennn  10429  seq3f1olemstep  10504  ser0  10517  exp3vallem  10524  facp1  10713  faclbnd  10724  bcn1  10741  hashennnuni  10762  hashcl  10764  hashfz1  10766  hashen  10767  fihashdom  10786  hashun  10788  zfz1isolem1  10823  zfz1iso  10824  sqrt0  11016  resqrexlemfp1  11021  cau3lem  11126  xrmaxifle  11257  xrmaxiflemval  11261  xrmaxltsup  11269  xrmaxadd  11272  climserle  11356  climcaucn  11362  iserabs  11486  isumshft  11501  cvgratgt0  11544  mertenslem2  11547  prodf1  11553  fprodunsn  11615  fprodfac  11626  eirrap  11788  bezoutlemzz  12006  dfgcd3  12014  nnmindc  12038  nnminle  12039  lcmcllem  12070  prmind2  12123  prm2orodd  12129  sqrt2irr0  12167  sqrt2irrap  12183  ennnfonelemjn  12406  ennnfonelemdm  12424  ennnfonelemim  12428  ctiunctlemfo  12443  isstructr  12480  basmex  12524  dfgrp2  12908  dfgrp3mlem  12974  grpissubg  13060  ablsubsub23  13134  lidlmex  13564  isbasis3g  13686  innei  13803  cnpnei  13859  cncnp2m  13871  cnptopresti  13878  cnptoprest2  13880  imasnopn  13939  xmettx  14150  cdivcncfap  14227  expcncf  14232  cnopnap  14234  ivthinclemdisj  14258  dvrecap  14317  2sqlem10  14612  ex-ceil  14618  bj-nnbist  14636  bj-con1st  14643  bj-charfunbi  14703  bj-sucexg  14814  bj-om  14829  bj-inf2vnlem1  14862  trilpolemisumle  14927  cndcap  14948