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  4270  undifexmid  4277  exmidn0m  4285  exmidsssn  4286  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  pocl  4394  sotritrieq  4416  frirrg  4441  unexg  4534  abnex  4538  reusv3i  4550  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  preleq  4647  0elsucexmid  4657  ordpwsucexmid  4662  ordtri2or2exmid  4663  elomssom  4697  brrelex12  4757  0nelrel  4765  elrel  4821  xpssres  5040  elres  5041  coi2  5245  iotabi  5288  uniabio  5289  nfunv  5351  funun  5362  funcnv3  5383  funimass1  5398  imain  5403  funssxp  5493  f0dom0  5519  f1o00  5608  fsn2  5809  funopsn  5817  isoselem  5944  oprabid  6033  brabvv  6050  uchoice  6283  oprssdmm  6317  1stdm  6328  f1o2ndf1  6374  poxp  6378  rdgon  6532  frecfcllem  6550  nntri3or  6639  nntri1  6642  ensym  6933  en2  6973  xpen  7006  snnen2oprc  7021  phplem4on  7029  fict  7030  fidceq  7031  infiexmid  7039  php5fin  7044  fisbth  7045  fin0  7047  fin0or  7048  diffisn  7055  infnfi  7057  en2eqpr  7069  exmidpw  7070  exmidpweq  7071  pw1fin  7072  fientri3  7077  unsnfi  7081  unsnfidcex  7082  unsnfidcel  7083  undifdcss  7085  ssfidc  7099  relcnvfi  7108  fiuni  7145  eqinfti  7187  djulclb  7222  updjud  7249  omp1eomlem  7261  0ct  7274  ctmlemr  7275  ctssdclemn0  7277  ctssdccl  7278  enomnilem  7305  finomni  7307  exmidomni  7309  enmkvlem  7328  enwomnilem  7336  exmidontriimlem1  7403  onntri35  7422  onntri52  7429  dftap2  7437  exmidapne  7446  enq0sym  7619  enq0tr  7621  prarloclem3  7684  nqprl  7738  nqpru  7739  addnqprlemrl  7744  addnqprlemru  7745  addnqprlemfl  7746  addnqprlemfu  7747  mulnqprlemrl  7760  mulnqprlemru  7761  mulnqprlemfl  7762  mulnqprlemfu  7763  ltexprlemfl  7796  ltexprlemfu  7798  recexprlemopl  7812  recexprlemopu  7814  aptipr  7828  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  caucvgprlemladdfu  7864  caucvgprprlemexbt  7893  suplocexprlemrl  7904  suplocexprlemru  7906  suplocexprlemex  7909  srpospr  7970  elrealeu  8016  axarch  8078  axcaucvglemres  8086  nn0ge2m1nn  9429  elnn0z  9459  peano2z  9482  uzm1  9753  qapne  9834  rpregt0  9863  rpnegap  9882  xnn0dcle  9998  xnn0letri  9999  npnflt  10011  nmnfgt  10014  xaddf  10040  xaddval  10041  xltadd1  10072  xsubge0  10077  xleaddadd  10083  elfz1end  10251  1fv  10335  elfzonlteqm1  10416  qtri3or  10460  exbtwnzlemshrink  10468  rebtwn2zlemshrink  10473  ioom  10480  elicore  10486  modfzo0difsn  10617  modsumfzodifsn  10618  addmodlteq  10620  frecfzennn  10648  seq3f1olemstep  10736  ser0  10755  exp3vallem  10762  facp1  10952  faclbnd  10963  bcn1  10980  hashennnuni  11001  hashcl  11003  hashfz1  11005  hashen  11006  fihashdom  11025  hashun  11027  zfz1isolem1  11062  zfz1iso  11063  lencl  11075  sswrd  11080  swrdswrd  11237  swrdccatin2  11261  pfxccat3  11266  pfxccatpfx1  11268  sqrt0  11515  resqrexlemfp1  11520  cau3lem  11625  xrmaxifle  11757  xrmaxiflemval  11761  xrmaxltsup  11769  xrmaxadd  11772  climserle  11856  climcaucn  11862  iserabs  11986  isumshft  12001  cvgratgt0  12044  mertenslem2  12047  prodf1  12053  fprodunsn  12115  fprodfac  12126  eirrap  12289  bezoutlemzz  12523  dfgcd3  12531  nnmindc  12555  nnminle  12556  nninfctlemfo  12561  lcmcllem  12589  prmind2  12642  prm2orodd  12648  sqrt2irr0  12686  sqrt2irrap  12702  ennnfonelemjn  12973  ennnfonelemdm  12991  ennnfonelemim  12995  ctiunctlemfo  13010  isstructr  13047  basmex  13092  dfgrp2  13560  dfgrp3mlem  13631  mulgnngsum  13664  grpissubg  13731  ablsubsub23  13862  rrgmex  14225  lssmex  14319  lidlmex  14439  2idlmex  14465  df2idl2  14473  2idlss  14478  isbasis3g  14720  innei  14837  cnpnei  14893  cncnp2m  14905  cnptopresti  14912  cnptoprest2  14914  imasnopn  14973  xmettx  15184  cdivcncfap  15278  expcncf  15283  cnopnap  15285  ivthinclemdisj  15314  dvrecap  15387  dvmptfsum  15399  gausslemma2dlem0i  15736  gausslemma2dlem1a  15737  2lgslem1c  15769  2sqlem10  15804  lfgredg2dom  15930  ausgrusgrben  15966  ausgrumgrien  15968  ausgrusgrien  15969  uspgredg2vlem  16018  uspgredg2v  16019  usgredg2vlem2  16021  ushgredgedg  16024  ushgredgedgloop  16026  wlk1walkdom  16070  wlk0prc  16083  ex-ceil  16090  bj-nnbist  16108  bj-con1st  16115  bj-charfunbi  16174  bj-sucexg  16285  bj-om  16300  bj-inf2vnlem1  16333  trilpolemisumle  16406  cndcap  16427