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  764  pm2.32  771  oranim  783  stabnot  835  exmiddc  838  pm2.1dc  839  stdcndcOLD  848  stdcn  849  const  854  imanst  890  pm5.75  965  rnlem  979  simp1bi  1015  simp2bi  1016  simp3bi  1017  syl3an1b  1286  syl3an2b  1287  syl3an3b  1288  exalim  1525  nford  1590  nfal  1599  stdpc5  1607  sbbii  1788  sb9i  2008  eu5  2101  exmoeudc  2117  eqeq1  2212  eleq2  2269  nner  2380  rexalim  2499  gencbvex  2819  gencbval  2821  moeq  2948  euind  2960  reuind  2978  ssel  3187  ssrmof  3256  unssd  3349  ssind  3397  unssdif  3408  ss0  3501  prprc  3743  disjnim  4035  trint  4158  snexprc  4231  undifexmid  4238  exmidn0m  4246  exmidsssn  4247  exmidundif  4251  exmidundifim  4252  exmid1stab  4253  pocl  4351  sotritrieq  4373  frirrg  4398  unexg  4491  abnex  4495  reusv3i  4507  ordtriexmid  4570  ontriexmidim  4571  ordtri2orexmid  4572  preleq  4604  0elsucexmid  4614  ordpwsucexmid  4619  ordtri2or2exmid  4620  elomssom  4654  brrelex12  4714  0nelrel  4722  elrel  4778  xpssres  4995  elres  4996  coi2  5200  iotabi  5242  uniabio  5243  nfunv  5305  funun  5316  funcnv3  5337  funimass1  5352  imain  5357  funssxp  5447  f0dom0  5471  f1o00  5559  fsn2  5756  funopsn  5764  isoselem  5891  oprabid  5978  brabvv  5993  uchoice  6225  oprssdmm  6259  1stdm  6270  f1o2ndf1  6316  poxp  6320  rdgon  6474  frecfcllem  6492  nntri3or  6581  nntri1  6584  ensym  6875  en2  6914  xpen  6944  snnen2oprc  6959  phplem4on  6966  fict  6967  fidceq  6968  infiexmid  6976  php5fin  6981  fisbth  6982  fin0  6984  fin0or  6985  diffisn  6992  infnfi  6994  en2eqpr  7006  exmidpw  7007  exmidpweq  7008  pw1fin  7009  fientri3  7014  unsnfi  7018  unsnfidcex  7019  unsnfidcel  7020  undifdcss  7022  ssfidc  7036  relcnvfi  7045  fiuni  7082  eqinfti  7124  djulclb  7159  updjud  7186  omp1eomlem  7198  0ct  7211  ctmlemr  7212  ctssdclemn0  7214  ctssdccl  7215  enomnilem  7242  finomni  7244  exmidomni  7246  enmkvlem  7265  enwomnilem  7273  exmidontriimlem1  7335  onntri35  7351  onntri52  7358  dftap2  7365  exmidapne  7374  enq0sym  7547  enq0tr  7549  prarloclem3  7612  nqprl  7666  nqpru  7667  addnqprlemrl  7672  addnqprlemru  7673  addnqprlemfl  7674  addnqprlemfu  7675  mulnqprlemrl  7688  mulnqprlemru  7689  mulnqprlemfl  7690  mulnqprlemfu  7691  ltexprlemfl  7724  ltexprlemfu  7726  recexprlemopl  7740  recexprlemopu  7742  aptipr  7756  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  caucvgprlemladdfu  7792  caucvgprprlemexbt  7821  suplocexprlemrl  7832  suplocexprlemru  7834  suplocexprlemex  7837  srpospr  7898  elrealeu  7944  axarch  8006  axcaucvglemres  8014  nn0ge2m1nn  9357  elnn0z  9387  peano2z  9410  uzm1  9681  qapne  9762  rpregt0  9791  rpnegap  9810  xnn0dcle  9926  xnn0letri  9927  npnflt  9939  nmnfgt  9942  xaddf  9968  xaddval  9969  xltadd1  10000  xsubge0  10005  xleaddadd  10011  elfz1end  10179  1fv  10263  elfzonlteqm1  10341  qtri3or  10385  exbtwnzlemshrink  10393  rebtwn2zlemshrink  10398  ioom  10405  elicore  10411  modfzo0difsn  10542  modsumfzodifsn  10543  addmodlteq  10545  frecfzennn  10573  seq3f1olemstep  10661  ser0  10680  exp3vallem  10687  facp1  10877  faclbnd  10888  bcn1  10905  hashennnuni  10926  hashcl  10928  hashfz1  10930  hashen  10931  fihashdom  10950  hashun  10952  zfz1isolem1  10987  zfz1iso  10988  lencl  11000  sswrd  11005  sqrt0  11348  resqrexlemfp1  11353  cau3lem  11458  xrmaxifle  11590  xrmaxiflemval  11594  xrmaxltsup  11602  xrmaxadd  11605  climserle  11689  climcaucn  11695  iserabs  11819  isumshft  11834  cvgratgt0  11877  mertenslem2  11880  prodf1  11886  fprodunsn  11948  fprodfac  11959  eirrap  12122  bezoutlemzz  12356  dfgcd3  12364  nnmindc  12388  nnminle  12389  nninfctlemfo  12394  lcmcllem  12422  prmind2  12475  prm2orodd  12481  sqrt2irr0  12519  sqrt2irrap  12535  ennnfonelemjn  12806  ennnfonelemdm  12824  ennnfonelemim  12828  ctiunctlemfo  12843  isstructr  12880  basmex  12924  dfgrp2  13392  dfgrp3mlem  13463  mulgnngsum  13496  grpissubg  13563  ablsubsub23  13694  rrgmex  14056  lssmex  14150  lidlmex  14270  2idlmex  14296  df2idl2  14304  2idlss  14309  isbasis3g  14551  innei  14668  cnpnei  14724  cncnp2m  14736  cnptopresti  14743  cnptoprest2  14745  imasnopn  14804  xmettx  15015  cdivcncfap  15109  expcncf  15114  cnopnap  15116  ivthinclemdisj  15145  dvrecap  15218  dvmptfsum  15230  gausslemma2dlem0i  15567  gausslemma2dlem1a  15568  2lgslem1c  15600  2sqlem10  15635  ex-ceil  15699  bj-nnbist  15717  bj-con1st  15724  bj-charfunbi  15784  bj-sucexg  15895  bj-om  15910  bj-inf2vnlem1  15943  trilpolemisumle  16014  cndcap  16035