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  1513  nford  1578  nfal  1587  stdpc5  1595  sbbii  1776  sb9i  1996  eu5  2089  exmoeudc  2105  eqeq1  2200  eleq2  2257  nner  2368  rexalim  2487  gencbvex  2807  gencbval  2809  moeq  2936  euind  2948  reuind  2966  ssel  3174  ssrmof  3243  unssd  3336  ssind  3384  unssdif  3395  ss0  3488  prprc  3729  disjnim  4021  trint  4143  snexprc  4216  undifexmid  4223  exmidn0m  4231  exmidsssn  4232  exmidundif  4236  exmidundifim  4237  exmid1stab  4238  pocl  4335  sotritrieq  4357  frirrg  4382  unexg  4475  abnex  4479  reusv3i  4491  ordtriexmid  4554  ontriexmidim  4555  ordtri2orexmid  4556  preleq  4588  0elsucexmid  4598  ordpwsucexmid  4603  ordtri2or2exmid  4604  elomssom  4638  brrelex12  4698  0nelrel  4706  elrel  4762  xpssres  4978  elres  4979  coi2  5183  iotabi  5225  uniabio  5226  nfunv  5288  funun  5299  funcnv3  5317  funimass1  5332  imain  5337  funssxp  5424  f0dom0  5448  f1o00  5536  fsn2  5733  isoselem  5864  oprabid  5951  brabvv  5965  uchoice  6192  oprssdmm  6226  1stdm  6237  f1o2ndf1  6283  poxp  6287  rdgon  6441  frecfcllem  6459  nntri3or  6548  nntri1  6551  ensym  6837  xpen  6903  snnen2oprc  6918  phplem4on  6925  fict  6926  fidceq  6927  infiexmid  6935  php5fin  6940  fisbth  6941  fin0  6943  fin0or  6944  diffisn  6951  infnfi  6953  en2eqpr  6965  exmidpw  6966  exmidpweq  6967  pw1fin  6968  fientri3  6973  unsnfi  6977  unsnfidcex  6978  unsnfidcel  6979  undifdcss  6981  ssfidc  6993  relcnvfi  7002  fiuni  7039  eqinfti  7081  djulclb  7116  updjud  7143  omp1eomlem  7155  0ct  7168  ctmlemr  7169  ctssdclemn0  7171  ctssdccl  7172  enomnilem  7199  finomni  7201  exmidomni  7203  enmkvlem  7222  enwomnilem  7230  exmidontriimlem1  7283  onntri35  7299  onntri52  7306  dftap2  7313  exmidapne  7322  enq0sym  7494  enq0tr  7496  prarloclem3  7559  nqprl  7613  nqpru  7614  addnqprlemrl  7619  addnqprlemru  7620  addnqprlemfl  7621  addnqprlemfu  7622  mulnqprlemrl  7635  mulnqprlemru  7636  mulnqprlemfl  7637  mulnqprlemfu  7638  ltexprlemfl  7671  ltexprlemfu  7673  recexprlemopl  7687  recexprlemopu  7689  aptipr  7703  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  caucvgprlemladdfu  7739  caucvgprprlemexbt  7768  suplocexprlemrl  7779  suplocexprlemru  7781  suplocexprlemex  7784  srpospr  7845  elrealeu  7891  axarch  7953  axcaucvglemres  7961  nn0ge2m1nn  9303  elnn0z  9333  peano2z  9356  uzm1  9626  qapne  9707  rpregt0  9736  rpnegap  9755  xnn0dcle  9871  xnn0letri  9872  npnflt  9884  nmnfgt  9887  xaddf  9913  xaddval  9914  xltadd1  9945  xsubge0  9950  xleaddadd  9956  elfz1end  10124  1fv  10208  elfzonlteqm1  10280  qtri3or  10313  exbtwnzlemshrink  10320  rebtwn2zlemshrink  10325  ioom  10332  elicore  10338  modfzo0difsn  10469  modsumfzodifsn  10470  addmodlteq  10472  frecfzennn  10500  seq3f1olemstep  10588  ser0  10607  exp3vallem  10614  facp1  10804  faclbnd  10815  bcn1  10832  hashennnuni  10853  hashcl  10855  hashfz1  10857  hashen  10858  fihashdom  10877  hashun  10879  zfz1isolem1  10914  zfz1iso  10915  lencl  10921  sswrd  10926  sqrt0  11151  resqrexlemfp1  11156  cau3lem  11261  xrmaxifle  11392  xrmaxiflemval  11396  xrmaxltsup  11404  xrmaxadd  11407  climserle  11491  climcaucn  11497  iserabs  11621  isumshft  11636  cvgratgt0  11679  mertenslem2  11682  prodf1  11688  fprodunsn  11750  fprodfac  11761  eirrap  11924  bezoutlemzz  12142  dfgcd3  12150  nnmindc  12174  nnminle  12175  nninfctlemfo  12180  lcmcllem  12208  prmind2  12261  prm2orodd  12267  sqrt2irr0  12305  sqrt2irrap  12321  ennnfonelemjn  12562  ennnfonelemdm  12580  ennnfonelemim  12584  ctiunctlemfo  12599  isstructr  12636  basmex  12680  dfgrp2  13102  dfgrp3mlem  13173  mulgnngsum  13200  grpissubg  13267  ablsubsub23  13398  rrgmex  13760  lssmex  13854  lidlmex  13974  2idlmex  14000  df2idl2  14008  2idlss  14013  isbasis3g  14225  innei  14342  cnpnei  14398  cncnp2m  14410  cnptopresti  14417  cnptoprest2  14419  imasnopn  14478  xmettx  14689  cdivcncfap  14783  expcncf  14788  cnopnap  14790  ivthinclemdisj  14819  dvrecap  14892  dvmptfsum  14904  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215  2lgslem1c  15247  2sqlem10  15282  ex-ceil  15288  bj-nnbist  15306  bj-con1st  15313  bj-charfunbi  15373  bj-sucexg  15484  bj-om  15499  bj-inf2vnlem1  15532  trilpolemisumle  15598  cndcap  15619