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  2034  eu5  2128  exmoeudc  2144  eqeq1  2239  eleq2  2296  nner  2416  rexalim  2535  gencbvex  2860  gencbval  2862  moeq  2991  euind  3003  reuind  3021  ssel  3231  ssrmof  3300  unssd  3394  ssind  3442  unssdif  3453  ss0  3546  rabsnif  3751  prprc  3795  disjnim  4092  trint  4216  snexprc  4291  undifexmid  4298  exmidn0m  4306  exmidsssn  4307  exmidundif  4311  exmidundifim  4312  exmid1stab  4313  pocl  4415  sotritrieq  4437  frirrg  4462  unexg  4555  abnex  4559  reusv3i  4571  ordtriexmid  4634  ontriexmidim  4635  ordtri2orexmid  4636  preleq  4668  0elsucexmid  4678  ordpwsucexmid  4683  ordtri2or2exmid  4684  elomssom  4718  brrelex12  4779  0nelrel  4787  elrel  4843  xpssres  5064  elres  5065  coi2  5270  iotabi  5313  uniabio  5314  nfunv  5376  funun  5388  funcnv3  5409  funimass1  5424  imain  5429  funssxp  5523  f0dom0  5552  f1o00  5642  fsn2  5842  funopsn  5851  isoselem  5984  oprabid  6073  brabvv  6090  uchoice  6322  oprssdmm  6356  1stdm  6367  f1o2ndf1  6415  poxp  6419  suppval1  6430  funsssuppss  6449  rdgon  6608  frecfcllem  6626  nntri3or  6717  nntri1  6720  ensym  7012  en2  7056  xpen  7089  snnen2oprc  7105  phplem4on  7113  fict  7114  fidceq  7115  infiexmid  7125  php5fin  7130  fisbth  7131  fin0  7133  fin0or  7134  diffisn  7141  infnfi  7143  fidcen  7147  en2eqpr  7158  exmidpw  7159  exmidpweq  7160  pw1fin  7161  fientri3  7166  unsnfi  7170  unsnfidcex  7171  unsnfidcel  7172  undifdcss  7174  ssfidc  7189  relcnvfi  7199  fiuni  7256  eqinfti  7302  djulclb  7337  updjud  7364  omp1eomlem  7376  0ct  7389  ctmlemr  7390  ctssdclemn0  7392  ctssdccl  7393  enomnilem  7420  finomni  7422  exmidomni  7424  enmkvlem  7443  enwomnilem  7451  exmidontriimlem1  7519  onntri35  7538  onntri52  7545  dftap2  7553  exmidapne  7562  enq0sym  7735  enq0tr  7737  prarloclem3  7800  nqprl  7854  nqpru  7855  addnqprlemrl  7860  addnqprlemru  7861  addnqprlemfl  7862  addnqprlemfu  7863  mulnqprlemrl  7876  mulnqprlemru  7877  mulnqprlemfl  7878  mulnqprlemfu  7879  ltexprlemfl  7912  ltexprlemfu  7914  recexprlemopl  7928  recexprlemopu  7930  aptipr  7944  cauappcvgprlemladdfu  7957  cauappcvgprlemladdfl  7958  caucvgprlemladdfu  7980  caucvgprprlemexbt  8009  suplocexprlemrl  8020  suplocexprlemru  8022  suplocexprlemex  8025  srpospr  8086  elrealeu  8132  axarch  8194  axcaucvglemres  8202  nn0ge2m1nn  9546  elnn0z  9576  peano2z  9599  uzm1  9871  qapne  9957  rpregt0  9986  rpnegap  10005  xnn0dcle  10121  xnn0letri  10122  npnflt  10134  nmnfgt  10137  xaddf  10163  xaddval  10164  xltadd1  10195  xsubge0  10200  xleaddadd  10206  elfz1end  10375  1fv  10459  elfzonlteqm1  10541  qtri3or  10586  exbtwnzlemshrink  10594  rebtwn2zlemshrink  10599  ioom  10606  elicore  10612  modfzo0difsn  10743  modsumfzodifsn  10744  addmodlteq  10746  frecfzennn  10774  seq3f1olemstep  10862  ser0  10881  exp3vallem  10888  facp1  11078  faclbnd  11089  bcn1  11106  hashennnuni  11127  hashcl  11129  hashfz1  11131  hashen  11132  fihashdom  11152  hashun  11154  zfz1isolem1  11190  zfz1iso  11191  lencl  11206  sswrd  11211  swrdswrd  11375  swrdccatin2  11399  pfxccat3  11404  pfxccatpfx1  11406  sqrt0  11667  resqrexlemfp1  11672  cau3lem  11777  xrmaxifle  11909  xrmaxiflemval  11913  xrmaxltsup  11921  xrmaxadd  11924  climserle  12008  climcaucn  12014  iserabs  12139  isumshft  12154  cvgratgt0  12197  mertenslem2  12200  prodf1  12206  fprodunsn  12268  fprodfac  12279  eirrap  12442  bezoutlemzz  12676  dfgcd3  12684  nnmindc  12708  nnminle  12709  nninfctlemfo  12714  lcmcllem  12742  prmind2  12795  prm2orodd  12801  sqrt2irr0  12839  sqrt2irrap  12855  ennnfonelemjn  13127  ennnfonelemdm  13145  ennnfonelemim  13149  ctiunctlemfo  13164  isstructr  13201  basmex  13246  dfgrp2  13714  dfgrp3mlem  13785  mulgnngsum  13818  grpissubg  13885  ablsubsub23  14016  rrgmex  14380  lssmex  14475  lidlmex  14595  2idlmex  14621  df2idl2  14629  2idlss  14634  isbasis3g  14881  innei  14998  cnpnei  15054  cncnp2m  15066  cnptopresti  15073  cnptoprest2  15075  imasnopn  15134  xmettx  15345  cdivcncfap  15439  expcncf  15444  cnopnap  15446  ivthinclemdisj  15475  dvrecap  15548  dvmptfsum  15560  gausslemma2dlem0i  15900  gausslemma2dlem1a  15901  2lgslem1c  15933  2sqlem10  15968  lfgredg2dom  16097  ausgrusgrben  16133  ausgrumgrien  16135  ausgrusgrien  16136  uspgredg2vlem  16185  uspgredg2v  16186  usgredg2vlem2  16188  ushgredgedg  16191  ushgredgedgloop  16193  griedg0ssusgr  16216  vtxedgfi  16254  vtxlpfi  16255  wlk1walkdom  16324  wlk0prc  16337  clwwlknonex2  16404  eupthi  16414  ex-ceil  16464  bj-nnbist  16486  bj-con1st  16493  bj-charfunbi  16551  bj-sucexg  16662  bj-om  16677  bj-inf2vnlem1  16710  trilpolemisumle  16792  cndcap  16814  gfsumval  16831