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  763  pm2.32  770  oranim  782  stabnot  834  exmiddc  837  pm2.1dc  838  stdcndcOLD  847  stdcn  848  const  853  imanst  889  pm5.75  964  rnlem  978  simp1bi  1014  simp2bi  1015  simp3bi  1016  syl3an1b  1285  syl3an2b  1286  syl3an3b  1287  exalim  1516  nford  1581  nfal  1590  stdpc5  1598  sbbii  1779  sb9i  1999  eu5  2092  exmoeudc  2108  eqeq1  2203  eleq2  2260  nner  2371  rexalim  2490  gencbvex  2810  gencbval  2812  moeq  2939  euind  2951  reuind  2969  ssel  3177  ssrmof  3246  unssd  3339  ssind  3387  unssdif  3398  ss0  3491  prprc  3732  disjnim  4024  trint  4146  snexprc  4219  undifexmid  4226  exmidn0m  4234  exmidsssn  4235  exmidundif  4239  exmidundifim  4240  exmid1stab  4241  pocl  4338  sotritrieq  4360  frirrg  4385  unexg  4478  abnex  4482  reusv3i  4494  ordtriexmid  4557  ontriexmidim  4558  ordtri2orexmid  4559  preleq  4591  0elsucexmid  4601  ordpwsucexmid  4606  ordtri2or2exmid  4607  elomssom  4641  brrelex12  4701  0nelrel  4709  elrel  4765  xpssres  4981  elres  4982  coi2  5186  iotabi  5228  uniabio  5229  nfunv  5291  funun  5302  funcnv3  5320  funimass1  5335  imain  5340  funssxp  5427  f0dom0  5451  f1o00  5539  fsn2  5736  isoselem  5867  oprabid  5954  brabvv  5968  uchoice  6195  oprssdmm  6229  1stdm  6240  f1o2ndf1  6286  poxp  6290  rdgon  6444  frecfcllem  6462  nntri3or  6551  nntri1  6554  ensym  6840  xpen  6906  snnen2oprc  6921  phplem4on  6928  fict  6929  fidceq  6930  infiexmid  6938  php5fin  6943  fisbth  6944  fin0  6946  fin0or  6947  diffisn  6954  infnfi  6956  en2eqpr  6968  exmidpw  6969  exmidpweq  6970  pw1fin  6971  fientri3  6976  unsnfi  6980  unsnfidcex  6981  unsnfidcel  6982  undifdcss  6984  ssfidc  6998  relcnvfi  7007  fiuni  7044  eqinfti  7086  djulclb  7121  updjud  7148  omp1eomlem  7160  0ct  7173  ctmlemr  7174  ctssdclemn0  7176  ctssdccl  7177  enomnilem  7204  finomni  7206  exmidomni  7208  enmkvlem  7227  enwomnilem  7235  exmidontriimlem1  7288  onntri35  7304  onntri52  7311  dftap2  7318  exmidapne  7327  enq0sym  7499  enq0tr  7501  prarloclem3  7564  nqprl  7618  nqpru  7619  addnqprlemrl  7624  addnqprlemru  7625  addnqprlemfl  7626  addnqprlemfu  7627  mulnqprlemrl  7640  mulnqprlemru  7641  mulnqprlemfl  7642  mulnqprlemfu  7643  ltexprlemfl  7676  ltexprlemfu  7678  recexprlemopl  7692  recexprlemopu  7694  aptipr  7708  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  caucvgprlemladdfu  7744  caucvgprprlemexbt  7773  suplocexprlemrl  7784  suplocexprlemru  7786  suplocexprlemex  7789  srpospr  7850  elrealeu  7896  axarch  7958  axcaucvglemres  7966  nn0ge2m1nn  9309  elnn0z  9339  peano2z  9362  uzm1  9632  qapne  9713  rpregt0  9742  rpnegap  9761  xnn0dcle  9877  xnn0letri  9878  npnflt  9890  nmnfgt  9893  xaddf  9919  xaddval  9920  xltadd1  9951  xsubge0  9956  xleaddadd  9962  elfz1end  10130  1fv  10214  elfzonlteqm1  10286  qtri3or  10330  exbtwnzlemshrink  10338  rebtwn2zlemshrink  10343  ioom  10350  elicore  10356  modfzo0difsn  10487  modsumfzodifsn  10488  addmodlteq  10490  frecfzennn  10518  seq3f1olemstep  10606  ser0  10625  exp3vallem  10632  facp1  10822  faclbnd  10833  bcn1  10850  hashennnuni  10871  hashcl  10873  hashfz1  10875  hashen  10876  fihashdom  10895  hashun  10897  zfz1isolem1  10932  zfz1iso  10933  lencl  10939  sswrd  10944  sqrt0  11169  resqrexlemfp1  11174  cau3lem  11279  xrmaxifle  11411  xrmaxiflemval  11415  xrmaxltsup  11423  xrmaxadd  11426  climserle  11510  climcaucn  11516  iserabs  11640  isumshft  11655  cvgratgt0  11698  mertenslem2  11701  prodf1  11707  fprodunsn  11769  fprodfac  11780  eirrap  11943  bezoutlemzz  12169  dfgcd3  12177  nnmindc  12201  nnminle  12202  nninfctlemfo  12207  lcmcllem  12235  prmind2  12288  prm2orodd  12294  sqrt2irr0  12332  sqrt2irrap  12348  ennnfonelemjn  12619  ennnfonelemdm  12637  ennnfonelemim  12641  ctiunctlemfo  12656  isstructr  12693  basmex  12737  dfgrp2  13159  dfgrp3mlem  13230  mulgnngsum  13257  grpissubg  13324  ablsubsub23  13455  rrgmex  13817  lssmex  13911  lidlmex  14031  2idlmex  14057  df2idl2  14065  2idlss  14070  isbasis3g  14282  innei  14399  cnpnei  14455  cncnp2m  14467  cnptopresti  14474  cnptoprest2  14476  imasnopn  14535  xmettx  14746  cdivcncfap  14840  expcncf  14845  cnopnap  14847  ivthinclemdisj  14876  dvrecap  14949  dvmptfsum  14961  gausslemma2dlem0i  15298  gausslemma2dlem1a  15299  2lgslem1c  15331  2sqlem10  15366  ex-ceil  15372  bj-nnbist  15390  bj-con1st  15397  bj-charfunbi  15457  bj-sucexg  15568  bj-om  15583  bj-inf2vnlem1  15616  trilpolemisumle  15682  cndcap  15703