Theorem biimpi 119

Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
biimpi.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
biimpi	⊢ (𝜑 → 𝜓)

Proof of Theorem biimpi

Step	Hyp	Ref	Expression
1		biimpi.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		bi1 117	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
3	1, 2	ax-mp 7	1 ⊢ (𝜑 → 𝜓)

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  270  simprbi  271  sylanb  280  sylan2b  283  anc2l  323  sylanblc  409  orbi2i  720  pm2.32  727  stabnot  784  imanst  785  exmiddc  788  pm2.1dc  789  oranim  851  stabtestimpdc  868  pm5.75  914  rnlem  928  simp1bi  964  simp2bi  965  simp3bi  966  syl3an1b  1220  syl3an2b  1221  syl3an3b  1222  exalim  1446  nford  1514  stdpc5  1531  sbbii  1706  sb9i  1916  eu5  2007  exmoeudc  2023  eqeq1  2106  eleq2  2163  nner  2271  rexalim  2389  gencbvex  2687  gencbval  2689  moeq  2812  euind  2824  reuind  2842  ssel  3041  unssd  3199  ssind  3247  unssdif  3258  ss0  3350  prprc  3580  disjnim  3866  trint  3981  snexprc  4050  undifexmid  4057  exmidn0m  4062  exmidsssn  4063  exmidundif  4067  exmidundifim  4068  pocl  4163  sotritrieq  4185  frirrg  4210  unexg  4302  abnex  4306  reusv3i  4318  ordtriexmid  4375  ordtri2orexmid  4376  preleq  4408  0elsucexmid  4418  ordpwsucexmid  4423  ordtri2or2exmid  4424  elnn  4457  brrelex12  4515  0nelrel  4523  elrel  4579  xpssres  4790  elres  4791  coi2  4991  iotabi  5033  uniabio  5034  nfunv  5092  funun  5103  funcnv3  5121  funimass1  5136  imain  5141  funssxp  5228  f0dom0  5252  f1o00  5336  fsn2  5526  isoselem  5653  oprabid  5735  brabvv  5749  1stdm  6010  f1o2ndf1  6055  poxp  6059  rdgon  6213  frecfcllem  6231  nntri3or  6319  nntri1  6322  ensym  6605  xpen  6668  snnen2oprc  6683  phplem4on  6690  fict  6691  fidceq  6692  infiexmid  6700  php5fin  6705  fisbth  6706  fin0  6708  fin0or  6709  diffisn  6716  infnfi  6718  en2eqpr  6730  exmidpw  6731  fientri3  6732  unsnfi  6736  unsnfidcex  6737  unsnfidcel  6738  undifdcss  6740  ssfidc  6751  relcnvfi  6757  eqinfti  6822  djulclb  6855  updjud  6882  omp1eomlem  6894  0ct  6907  ctmlemr  6908  ctssdclemn0  6910  ctssdclemr  6911  enomnilem  6922  finomni  6924  exmidomni  6926  enq0sym  7141  enq0tr  7143  prarloclem3  7206  nqprl  7260  nqpru  7261  addnqprlemrl  7266  addnqprlemru  7267  addnqprlemfl  7268  addnqprlemfu  7269  mulnqprlemrl  7282  mulnqprlemru  7283  mulnqprlemfl  7284  mulnqprlemfu  7285  ltexprlemfl  7318  ltexprlemfu  7320  recexprlemopl  7334  recexprlemopu  7336  aptipr  7350  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  caucvgprlemladdfu  7386  caucvgprprlemexbt  7415  srpospr  7478  elrealeu  7517  axarch  7576  axcaucvglemres  7584  nn0ge2m1nn  8889  elnn0z  8919  peano2z  8942  uzm1  9206  qapne  9281  rpregt0  9304  rpnegap  9323  npnflt  9439  nmnfgt  9442  xaddf  9468  xaddval  9469  xltadd1  9500  xsubge0  9505  xleaddadd  9511  elfz1end  9676  1fv  9757  elfzonlteqm1  9828  qtri3or  9861  exbtwnzlemshrink  9867  rebtwn2zlemshrink  9872  ioom  9879  modfzo0difsn  10009  modsumfzodifsn  10010  addmodlteq  10012  frecfzennn  10040  seq3f1olemstep  10115  ser0  10128  exp3vallem  10135  facp1  10317  faclbnd  10328  bcn1  10345  hashennnuni  10366  hashcl  10368  hashfz1  10370  hashen  10371  fihashdom  10390  hashun  10392  zfz1isolem1  10424  zfz1iso  10425  sqrt0  10616  resqrexlemfp1  10621  cau3lem  10726  xrmaxifle  10854  xrmaxiflemval  10858  xrmaxltsup  10866  xrmaxadd  10869  climserle  10953  climcaucn  10959  iserabs  11083  isumshft  11098  cvgratgt0  11141  mertenslem2  11144  eirrap  11279  bezoutlemzz  11483  dfgcd3  11491  lcmcllem  11541  prmind2  11594  prm2orodd  11600  sqrt2irrap  11650  ennnfonelemjn  11707  ennnfonelemdm  11725  ennnfonelemim  11729  isstructr  11756  isbasis3g  11995  innei  12114  cnpnei  12169  cncnp2m  12181  cnptopresti  12188  cnptoprest2  12190  imasnopn  12249  cdivcncfap  12499  expcncf  12504  ex-ceil  12541  bj-sucexg  12701  bj-om  12720  bj-inf2vnlem1  12753  trilpolemisumle  12815