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  770  pm2.32  777  oranim  789  stabnot  841  exmiddc  844  pm2.1dc  845  stdcndcOLD  854  stdcn  855  const  860  imanst  896  pm5.75  971  rnlem  985  ifpnst  997  simp1bi  1039  simp2bi  1040  simp3bi  1041  syl3an1b  1310  syl3an2b  1311  syl3an3b  1312  exalim  1551  nford  1616  nfal  1625  stdpc5  1633  sbbii  1814  sb9i  2036  eu5  2130  exmoeudc  2146  eqeq1  2241  eleq2  2298  nner  2418  rexalim  2537  gencbvex  2863  gencbval  2865  moeq  2994  euind  3006  reuind  3024  ssel  3234  ssrmof  3303  unssd  3397  ssind  3447  unssdif  3458  ss0  3551  rabsnif  3760  prprc  3804  disjnim  4101  trint  4225  snexprc  4301  undifexmid  4308  exmidn0m  4316  exmidsssn  4317  exmidundif  4321  exmidundifim  4322  exmid1stab  4323  pocl  4426  sotritrieq  4448  frirrg  4473  unexg  4566  abnex  4570  reusv3i  4582  ordtriexmid  4645  ontriexmidim  4646  ordtri2orexmid  4647  preleq  4679  0elsucexmid  4689  ordpwsucexmid  4694  ordtri2or2exmid  4695  elomssom  4729  brrelex12  4790  0nelrel  4798  elrel  4854  xpssres  5075  elres  5076  coi2  5281  iotabi  5324  uniabio  5325  nfunv  5387  funun  5399  funcnv3  5420  funimass1  5435  imain  5440  funssxp  5534  f0dom0  5563  f1o00  5653  fsn2  5853  funopsn  5862  isoselem  5995  oprabid  6084  brabvv  6101  uchoice  6333  oprssdmm  6367  1stdm  6378  f1o2ndf1  6426  poxp  6430  suppval1  6441  funsssuppss  6460  rdgon  6619  frecfcllem  6637  nntri3or  6728  nntri1  6731  ensym  7023  en2  7067  xpen  7100  snnen2oprc  7116  phplem4on  7124  fict  7125  fidceq  7126  infiexmid  7136  php5fin  7141  fisbth  7142  fin0  7144  fin0or  7145  diffisn  7152  infnfi  7154  fidcen  7158  en2eqpr  7169  exmidpw  7170  exmidpweq  7171  pw1fin  7172  fientri3  7177  unsnfi  7181  unsnfidcex  7182  unsnfidcel  7183  undifdcss  7185  ssfidc  7200  relcnvfi  7210  fiuni  7267  eqinfti  7313  djulclb  7348  updjud  7375  omp1eomlem  7387  0ct  7400  ctmlemr  7401  ctssdclemn0  7403  ctssdccl  7404  enomnilem  7431  finomni  7433  exmidomni  7435  enmkvlem  7454  enwomnilem  7462  exmidontriimlem1  7530  onntri35  7549  onntri52  7556  dftap2  7567  exmidapne  7576  enq0sym  7749  enq0tr  7751  prarloclem3  7814  nqprl  7868  nqpru  7869  addnqprlemrl  7874  addnqprlemru  7875  addnqprlemfl  7876  addnqprlemfu  7877  mulnqprlemrl  7890  mulnqprlemru  7891  mulnqprlemfl  7892  mulnqprlemfu  7893  ltexprlemfl  7926  ltexprlemfu  7928  recexprlemopl  7942  recexprlemopu  7944  aptipr  7958  cauappcvgprlemladdfu  7971  cauappcvgprlemladdfl  7972  caucvgprlemladdfu  7994  caucvgprprlemexbt  8023  suplocexprlemrl  8034  suplocexprlemru  8036  suplocexprlemex  8039  srpospr  8100  elrealeu  8146  axarch  8208  axcaucvglemres  8216  nn0ge2m1nn  9562  elnn0z  9592  peano2z  9615  uzm1  9888  qapne  9974  rpregt0  10003  rpnegap  10022  xnn0dcle  10138  xnn0letri  10139  npnflt  10151  nmnfgt  10154  xaddf  10180  xaddval  10181  xltadd1  10212  xsubge0  10217  xleaddadd  10223  elfz1end  10392  1fv  10477  elfzonlteqm1  10559  qtri3or  10604  exbtwnzlemshrink  10612  rebtwn2zlemshrink  10617  ioom  10624  elicore  10630  modfzo0difsn  10761  modsumfzodifsn  10762  addmodlteq  10764  frecfzennn  10792  seq3f1olemstep  10880  ser0  10899  exp3vallem  10906  facp1  11096  faclbnd  11107  bcn1  11124  hashennnuni  11146  hashcl  11148  hashfz1  11150  hashen  11151  fihashdom  11171  hashun  11173  zfz1isolem1  11216  zfz1iso  11217  lencl  11232  sswrd  11237  swrdswrd  11401  swrdccatin2  11425  pfxccat3  11430  pfxccatpfx1  11432  sqrt0  11693  resqrexlemfp1  11698  cau3lem  11803  xrmaxifle  11935  xrmaxiflemval  11939  xrmaxltsup  11947  xrmaxadd  11950  climserle  12034  climcaucn  12040  iserabs  12165  isumshft  12180  cvgratgt0  12223  mertenslem2  12226  prodf1  12232  fprodunsn  12294  fprodfac  12305  eirrap  12468  bezoutlemzz  12702  dfgcd3  12710  nnmindc  12734  nnminle  12735  nninfctlemfo  12740  lcmcllem  12768  prmind2  12821  prm2orodd  12827  sqrt2irr0  12865  sqrt2irrap  12881  ballotfilem2  13149  ennnfonelemjn  13170  ennnfonelemdm  13188  ennnfonelemim  13192  ctiunctlemfo  13207  isstructr  13244  basmex  13289  dfgrp2  13757  dfgrp3mlem  13828  mulgnngsum  13861  grpissubg  13928  ablsubsub23  14059  rrgmex  14423  lssmex  14520  lidlmex  14640  2idlmex  14666  df2idl2  14674  2idlss  14679  isbasis3g  14928  innei  15045  cnpnei  15101  cncnp2m  15113  cnptopresti  15120  cnptoprest2  15122  imasnopn  15181  xmettx  15392  cdivcncfap  15486  expcncf  15491  cnopnap  15493  ivthinclemdisj  15522  dvrecap  15595  dvmptfsum  15607  gausslemma2dlem0i  15947  gausslemma2dlem1a  15948  2lgslem1c  15980  2sqlem10  16015  lfgredg2dom  16144  ausgrusgrben  16180  ausgrumgrien  16182  ausgrusgrien  16183  uspgredg2vlem  16232  uspgredg2v  16233  usgredg2vlem2  16235  ushgredgedg  16238  ushgredgedgloop  16240  griedg0ssusgr  16263  vtxedgfi  16301  vtxlpfi  16302  wlk1walkdom  16371  wlk0prc  16384  clwwlknonex2  16451  eupthi  16461  ex-ceil  16511  bj-nnbist  16533  bj-con1st  16540  bj-charfunbi  16598  bj-sucexg  16709  bj-om  16724  bj-inf2vnlem1  16757  trilpolemisumle  16839  cndcap  16861  trimul0or  16862  gfsumval  16879