Theorem biimpi 119

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		bi1 117	. 2 |- ( ( ph <-> ps ) -> ( ph -> ps ) )
3	1, 2	ax-mp 7	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbi  120  sylib  121  sylbb  122  biimpri  132  mpbi  144  syl5bi  151  syl6ib  160  syl7bi  164  syl8ib  165  bitri  183  simplbi  269  simprbi  270  sylanb  279  sylan2b  282  anc2l  321  sylanblc  407  orbi2i  715  pm2.32  722  stabnot  779  imanst  780  exmiddc  783  pm2.1dc  784  oranim  846  stabtestimpdc  863  pm5.75  909  rnlem  923  simp1bi  959  simp2bi  960  simp3bi  961  syl3an1b  1211  syl3an2b  1212  syl3an3b  1213  exalim  1437  nford  1505  stdpc5  1522  sbbii  1696  sb9i  1905  eu5  1996  exmoeudc  2012  eqeq1  2095  eleq2  2152  nner  2260  rexalim  2374  gencbvex  2666  gencbval  2668  moeq  2791  euind  2803  reuind  2821  ssel  3020  unssd  3177  ssind  3225  unssdif  3235  ss0  3327  prprc  3556  disjnim  3842  trint  3957  snexprc  4027  undifexmid  4034  exmidn0m  4039  exmidsssn  4040  exmidundif  4043  exmidundifim  4044  pocl  4139  sotritrieq  4161  frirrg  4186  unexg  4278  abnex  4282  reusv3i  4294  ordtriexmid  4351  ordtri2orexmid  4352  preleq  4384  0elsucexmid  4394  ordpwsucexmid  4399  ordtri2or2exmid  4400  elnn  4433  brrelex12  4489  0nelrel  4497  elrel  4553  xpssres  4760  elres  4761  coi2  4960  iotabi  5002  uniabio  5003  nfunv  5060  funun  5071  funcnv3  5089  funimass1  5104  imain  5109  funssxp  5193  f0dom0  5217  f1o00  5301  fsn2  5485  isoselem  5613  oprabid  5695  brabvv  5709  1stdm  5966  f1o2ndf1  6007  poxp  6011  rdgon  6165  frecfcllem  6183  nntri3or  6268  nntri1  6271  ensym  6552  xpen  6615  snnen2oprc  6630  phplem4on  6637  fict  6638  fidceq  6639  infiexmid  6647  php5fin  6652  fisbth  6653  fin0  6655  fin0or  6656  diffisn  6663  infnfi  6665  en2eqpr  6677  exmidpw  6678  fientri3  6679  unsnfi  6683  unsnfidcex  6684  unsnfidcel  6685  undifdcss  6687  ssfidc  6698  relcnvfi  6704  eqinfti  6769  djulclb  6801  enomnilem  6855  finomni  6857  exmidomni  6859  enq0sym  7052  enq0tr  7054  prarloclem3  7117  nqprl  7171  nqpru  7172  addnqprlemrl  7177  addnqprlemru  7178  addnqprlemfl  7179  addnqprlemfu  7180  mulnqprlemrl  7193  mulnqprlemru  7194  mulnqprlemfl  7195  mulnqprlemfu  7196  ltexprlemfl  7229  ltexprlemfu  7231  recexprlemopl  7245  recexprlemopu  7247  aptipr  7261  cauappcvgprlemladdfu  7274  cauappcvgprlemladdfl  7275  caucvgprlemladdfu  7297  caucvgprprlemexbt  7326  srpospr  7389  elrealeu  7428  axarch  7487  axcaucvglemres  7495  nn0ge2m1nn  8794  elnn0z  8824  peano2z  8847  uzm1  9110  qapne  9185  rpregt0  9208  rpnegap  9227  elfz1end  9530  1fv  9611  elfzonlteqm1  9682  qtri3or  9715  exbtwnzlemshrink  9721  rebtwn2zlemshrink  9726  ioom  9733  modfzo0difsn  9863  modsumfzodifsn  9864  addmodlteq  9866  frecfzennn  9894  seq3f1olemstep  9991  iser0  10008  ser0  10010  exp3vallem  10017  facp1  10199  faclbnd  10210  bcn1  10227  hashennnuni  10248  hashcl  10250  hashfz1  10252  hashen  10253  fihashdom  10272  hashun  10274  zfz1isolem1  10306  zfz1iso  10307  sqrt0  10498  resqrexlemfp1  10503  cau3lem  10608  climserle  10795  climcaucn  10801  iserabs  10930  isumshft  10945  cvgratgt0  10988  mertenslem2  10991  eirrap  11126  bezoutlemzz  11330  dfgcd3  11338  lcmcllem  11388  prmind2  11441  prm2orodd  11447  sqrt2irrap  11497  isstructr  11570  isbasis3g  11805  ex-ceil  11926  bj-sucexg  12086  bj-om  12105  bj-inf2vnlem1  12138