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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 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  272  simprbi  273  sylanb  282  sylan2b  285  anc2l  325  sylanblc  412  orbi2i  752  pm2.32  759  oranim  771  stabnot  823  exmiddc  826  pm2.1dc  827  stdcndcOLD  836  stdcn  837  const  842  imanst  878  pm5.75  952  rnlem  966  simp1bi  1002  simp2bi  1003  simp3bi  1004  syl3an1b  1264  syl3an2b  1265  syl3an3b  1266  exalim  1490  nford  1555  nfal  1564  stdpc5  1572  sbbii  1753  sb9i  1968  eu5  2061  exmoeudc  2077  eqeq1  2172  eleq2  2229  nner  2339  rexalim  2458  gencbvex  2771  gencbval  2773  moeq  2900  euind  2912  reuind  2930  ssel  3135  ssrmof  3204  unssd  3297  ssind  3345  unssdif  3356  ss0  3448  prprc  3685  disjnim  3972  trint  4094  snexprc  4164  undifexmid  4171  exmidn0m  4179  exmidsssn  4180  exmidundif  4184  exmidundifim  4185  pocl  4280  sotritrieq  4302  frirrg  4327  unexg  4420  abnex  4424  reusv3i  4436  ordtriexmid  4497  ontriexmidim  4498  ordtri2orexmid  4499  preleq  4531  0elsucexmid  4541  ordpwsucexmid  4546  ordtri2or2exmid  4547  elomssom  4581  brrelex12  4641  0nelrel  4649  elrel  4705  xpssres  4918  elres  4919  coi2  5119  iotabi  5161  uniabio  5162  nfunv  5220  funun  5231  funcnv3  5249  funimass1  5264  imain  5269  funssxp  5356  f0dom0  5380  f1o00  5466  fsn2  5658  isoselem  5787  oprabid  5870  brabvv  5884  oprssdmm  6136  1stdm  6147  f1o2ndf1  6192  poxp  6196  rdgon  6350  frecfcllem  6368  nntri3or  6457  nntri1  6460  ensym  6743  xpen  6807  snnen2oprc  6822  phplem4on  6829  fict  6830  fidceq  6831  infiexmid  6839  php5fin  6844  fisbth  6845  fin0  6847  fin0or  6848  diffisn  6855  infnfi  6857  en2eqpr  6869  exmidpw  6870  exmidpweq  6871  pw1fin  6872  fientri3  6876  unsnfi  6880  unsnfidcex  6881  unsnfidcel  6882  undifdcss  6884  ssfidc  6896  relcnvfi  6902  fiuni  6939  eqinfti  6981  djulclb  7016  updjud  7043  omp1eomlem  7055  0ct  7068  ctmlemr  7069  ctssdclemn0  7071  ctssdccl  7072  enomnilem  7098  finomni  7100  exmidomni  7102  enmkvlem  7121  enwomnilem  7129  exmidontriimlem1  7173  onntri35  7189  onntri52  7196  enq0sym  7369  enq0tr  7371  prarloclem3  7434  nqprl  7488  nqpru  7489  addnqprlemrl  7494  addnqprlemru  7495  addnqprlemfl  7496  addnqprlemfu  7497  mulnqprlemrl  7510  mulnqprlemru  7511  mulnqprlemfl  7512  mulnqprlemfu  7513  ltexprlemfl  7546  ltexprlemfu  7548  recexprlemopl  7562  recexprlemopu  7564  aptipr  7578  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  caucvgprlemladdfu  7614  caucvgprprlemexbt  7643  suplocexprlemrl  7654  suplocexprlemru  7656  suplocexprlemex  7659  srpospr  7720  elrealeu  7766  axarch  7828  axcaucvglemres  7836  nn0ge2m1nn  9170  elnn0z  9200  peano2z  9223  uzm1  9492  qapne  9573  rpregt0  9599  rpnegap  9618  xnn0dcle  9734  xnn0letri  9735  npnflt  9747  nmnfgt  9750  xaddf  9776  xaddval  9777  xltadd1  9808  xsubge0  9813  xleaddadd  9819  elfz1end  9986  1fv  10070  elfzonlteqm1  10141  qtri3or  10174  exbtwnzlemshrink  10180  rebtwn2zlemshrink  10185  ioom  10192  elicore  10198  modfzo0difsn  10326  modsumfzodifsn  10327  addmodlteq  10329  frecfzennn  10357  seq3f1olemstep  10432  ser0  10445  exp3vallem  10452  facp1  10639  faclbnd  10650  bcn1  10667  hashennnuni  10688  hashcl  10690  hashfz1  10692  hashen  10693  fihashdom  10712  hashun  10714  zfz1isolem1  10749  zfz1iso  10750  sqrt0  10942  resqrexlemfp1  10947  cau3lem  11052  xrmaxifle  11183  xrmaxiflemval  11187  xrmaxltsup  11195  xrmaxadd  11198  climserle  11282  climcaucn  11288  iserabs  11412  isumshft  11427  cvgratgt0  11470  mertenslem2  11473  prodf1  11479  fprodunsn  11541  fprodfac  11552  eirrap  11714  bezoutlemzz  11931  dfgcd3  11939  nnmindc  11963  nnminle  11964  lcmcllem  11995  prmind2  12048  prm2orodd  12054  sqrt2irr0  12092  sqrt2irrap  12108  ennnfonelemjn  12331  ennnfonelemdm  12349  ennnfonelemim  12353  ctiunctlemfo  12368  isstructr  12405  isbasis3g  12644  innei  12763  cnpnei  12819  cncnp2m  12831  cnptopresti  12838  cnptoprest2  12840  imasnopn  12899  xmettx  13110  cdivcncfap  13187  expcncf  13192  cnopnap  13194  ivthinclemdisj  13218  dvrecap  13277  2sqlem10  13561  ex-ceil  13567  bj-nnbist  13585  bj-con1st  13592  bj-charfunbi  13653  bj-sucexg  13764  bj-om  13779  bj-inf2vnlem1  13812  exmid1stab  13840  trilpolemisumle  13877