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  5495  f0dom0  5521  f1o00  5610  fsn2  5811  funopsn  5819  isoselem  5950  oprabid  6039  brabvv  6056  uchoice  6289  oprssdmm  6323  1stdm  6334  f1o2ndf1  6380  poxp  6384  rdgon  6538  frecfcllem  6556  nntri3or  6647  nntri1  6650  ensym  6941  en2  6981  xpen  7014  snnen2oprc  7029  phplem4on  7037  fict  7038  fidceq  7039  infiexmid  7047  php5fin  7052  fisbth  7053  fin0  7055  fin0or  7056  diffisn  7063  infnfi  7065  fidcen  7069  en2eqpr  7080  exmidpw  7081  exmidpweq  7082  pw1fin  7083  fientri3  7088  unsnfi  7092  unsnfidcex  7093  unsnfidcel  7094  undifdcss  7096  ssfidc  7110  relcnvfi  7119  fiuni  7156  eqinfti  7198  djulclb  7233  updjud  7260  omp1eomlem  7272  0ct  7285  ctmlemr  7286  ctssdclemn0  7288  ctssdccl  7289  enomnilem  7316  finomni  7318  exmidomni  7320  enmkvlem  7339  enwomnilem  7347  exmidontriimlem1  7414  onntri35  7433  onntri52  7440  dftap2  7448  exmidapne  7457  enq0sym  7630  enq0tr  7632  prarloclem3  7695  nqprl  7749  nqpru  7750  addnqprlemrl  7755  addnqprlemru  7756  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemrl  7771  mulnqprlemru  7772  mulnqprlemfl  7773  mulnqprlemfu  7774  ltexprlemfl  7807  ltexprlemfu  7809  recexprlemopl  7823  recexprlemopu  7825  aptipr  7839  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  caucvgprlemladdfu  7875  caucvgprprlemexbt  7904  suplocexprlemrl  7915  suplocexprlemru  7917  suplocexprlemex  7920  srpospr  7981  elrealeu  8027  axarch  8089  axcaucvglemres  8097  nn0ge2m1nn  9440  elnn0z  9470  peano2z  9493  uzm1  9765  qapne  9846  rpregt0  9875  rpnegap  9894  xnn0dcle  10010  xnn0letri  10011  npnflt  10023  nmnfgt  10026  xaddf  10052  xaddval  10053  xltadd1  10084  xsubge0  10089  xleaddadd  10095  elfz1end  10263  1fv  10347  elfzonlteqm1  10428  qtri3or  10472  exbtwnzlemshrink  10480  rebtwn2zlemshrink  10485  ioom  10492  elicore  10498  modfzo0difsn  10629  modsumfzodifsn  10630  addmodlteq  10632  frecfzennn  10660  seq3f1olemstep  10748  ser0  10767  exp3vallem  10774  facp1  10964  faclbnd  10975  bcn1  10992  hashennnuni  11013  hashcl  11015  hashfz1  11017  hashen  11018  fihashdom  11037  hashun  11039  zfz1isolem1  11075  zfz1iso  11076  lencl  11088  sswrd  11093  swrdswrd  11253  swrdccatin2  11277  pfxccat3  11282  pfxccatpfx1  11284  sqrt0  11531  resqrexlemfp1  11536  cau3lem  11641  xrmaxifle  11773  xrmaxiflemval  11777  xrmaxltsup  11785  xrmaxadd  11788  climserle  11872  climcaucn  11878  iserabs  12002  isumshft  12017  cvgratgt0  12060  mertenslem2  12063  prodf1  12069  fprodunsn  12131  fprodfac  12142  eirrap  12305  bezoutlemzz  12539  dfgcd3  12547  nnmindc  12571  nnminle  12572  nninfctlemfo  12577  lcmcllem  12605  prmind2  12658  prm2orodd  12664  sqrt2irr0  12702  sqrt2irrap  12718  ennnfonelemjn  12989  ennnfonelemdm  13007  ennnfonelemim  13011  ctiunctlemfo  13026  isstructr  13063  basmex  13108  dfgrp2  13576  dfgrp3mlem  13647  mulgnngsum  13680  grpissubg  13747  ablsubsub23  13878  rrgmex  14241  lssmex  14335  lidlmex  14455  2idlmex  14481  df2idl2  14489  2idlss  14494  isbasis3g  14736  innei  14853  cnpnei  14909  cncnp2m  14921  cnptopresti  14928  cnptoprest2  14930  imasnopn  14989  xmettx  15200  cdivcncfap  15294  expcncf  15299  cnopnap  15301  ivthinclemdisj  15330  dvrecap  15403  dvmptfsum  15415  gausslemma2dlem0i  15752  gausslemma2dlem1a  15753  2lgslem1c  15785  2sqlem10  15820  lfgredg2dom  15946  ausgrusgrben  15982  ausgrumgrien  15984  ausgrusgrien  15985  uspgredg2vlem  16034  uspgredg2v  16035  usgredg2vlem2  16037  ushgredgedg  16040  ushgredgedgloop  16042  vtxedgfi  16049  vtxlpfi  16050  wlk1walkdom  16105  wlk0prc  16118  ex-ceil  16173  bj-nnbist  16191  bj-con1st  16198  bj-charfunbi  16257  bj-sucexg  16368  bj-om  16383  bj-inf2vnlem1  16416  trilpolemisumle  16494  cndcap  16515