Theorem biimpi 120

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		biimp 118	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 → 𝜓)

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  3178  ssrmof  3247  unssd  3340  ssind  3388  unssdif  3399  ss0  3492  prprc  3733  disjnim  4025  trint  4147  snexprc  4220  undifexmid  4227  exmidn0m  4235  exmidsssn  4236  exmidundif  4240  exmidundifim  4241  exmid1stab  4242  pocl  4339  sotritrieq  4361  frirrg  4386  unexg  4479  abnex  4483  reusv3i  4495  ordtriexmid  4558  ontriexmidim  4559  ordtri2orexmid  4560  preleq  4592  0elsucexmid  4602  ordpwsucexmid  4607  ordtri2or2exmid  4608  elomssom  4642  brrelex12  4702  0nelrel  4710  elrel  4766  xpssres  4982  elres  4983  coi2  5187  iotabi  5229  uniabio  5230  nfunv  5292  funun  5303  funcnv3  5321  funimass1  5336  imain  5341  funssxp  5430  f0dom0  5454  f1o00  5542  fsn2  5739  isoselem  5870  oprabid  5957  brabvv  5972  uchoice  6204  oprssdmm  6238  1stdm  6249  f1o2ndf1  6295  poxp  6299  rdgon  6453  frecfcllem  6471  nntri3or  6560  nntri1  6563  ensym  6849  xpen  6915  snnen2oprc  6930  phplem4on  6937  fict  6938  fidceq  6939  infiexmid  6947  php5fin  6952  fisbth  6953  fin0  6955  fin0or  6956  diffisn  6963  infnfi  6965  en2eqpr  6977  exmidpw  6978  exmidpweq  6979  pw1fin  6980  fientri3  6985  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  undifdcss  6993  ssfidc  7007  relcnvfi  7016  fiuni  7053  eqinfti  7095  djulclb  7130  updjud  7157  omp1eomlem  7169  0ct  7182  ctmlemr  7183  ctssdclemn0  7185  ctssdccl  7186  enomnilem  7213  finomni  7215  exmidomni  7217  enmkvlem  7236  enwomnilem  7244  exmidontriimlem1  7306  onntri35  7322  onntri52  7329  dftap2  7336  exmidapne  7345  enq0sym  7518  enq0tr  7520  prarloclem3  7583  nqprl  7637  nqpru  7638  addnqprlemrl  7643  addnqprlemru  7644  addnqprlemfl  7645  addnqprlemfu  7646  mulnqprlemrl  7659  mulnqprlemru  7660  mulnqprlemfl  7661  mulnqprlemfu  7662  ltexprlemfl  7695  ltexprlemfu  7697  recexprlemopl  7711  recexprlemopu  7713  aptipr  7727  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  caucvgprlemladdfu  7763  caucvgprprlemexbt  7792  suplocexprlemrl  7803  suplocexprlemru  7805  suplocexprlemex  7808  srpospr  7869  elrealeu  7915  axarch  7977  axcaucvglemres  7985  nn0ge2m1nn  9328  elnn0z  9358  peano2z  9381  uzm1  9651  qapne  9732  rpregt0  9761  rpnegap  9780  xnn0dcle  9896  xnn0letri  9897  npnflt  9909  nmnfgt  9912  xaddf  9938  xaddval  9939  xltadd1  9970  xsubge0  9975  xleaddadd  9981  elfz1end  10149  1fv  10233  elfzonlteqm1  10305  qtri3or  10349  exbtwnzlemshrink  10357  rebtwn2zlemshrink  10362  ioom  10369  elicore  10375  modfzo0difsn  10506  modsumfzodifsn  10507  addmodlteq  10509  frecfzennn  10537  seq3f1olemstep  10625  ser0  10644  exp3vallem  10651  facp1  10841  faclbnd  10852  bcn1  10869  hashennnuni  10890  hashcl  10892  hashfz1  10894  hashen  10895  fihashdom  10914  hashun  10916  zfz1isolem1  10951  zfz1iso  10952  lencl  10958  sswrd  10963  sqrt0  11188  resqrexlemfp1  11193  cau3lem  11298  xrmaxifle  11430  xrmaxiflemval  11434  xrmaxltsup  11442  xrmaxadd  11445  climserle  11529  climcaucn  11535  iserabs  11659  isumshft  11674  cvgratgt0  11717  mertenslem2  11720  prodf1  11726  fprodunsn  11788  fprodfac  11799  eirrap  11962  bezoutlemzz  12196  dfgcd3  12204  nnmindc  12228  nnminle  12229  nninfctlemfo  12234  lcmcllem  12262  prmind2  12315  prm2orodd  12321  sqrt2irr0  12359  sqrt2irrap  12375  ennnfonelemjn  12646  ennnfonelemdm  12664  ennnfonelemim  12668  ctiunctlemfo  12683  isstructr  12720  basmex  12764  dfgrp2  13231  dfgrp3mlem  13302  mulgnngsum  13335  grpissubg  13402  ablsubsub23  13533  rrgmex  13895  lssmex  13989  lidlmex  14109  2idlmex  14135  df2idl2  14143  2idlss  14148  isbasis3g  14390  innei  14507  cnpnei  14563  cncnp2m  14575  cnptopresti  14582  cnptoprest2  14584  imasnopn  14643  xmettx  14854  cdivcncfap  14948  expcncf  14953  cnopnap  14955  ivthinclemdisj  14984  dvrecap  15057  dvmptfsum  15069  gausslemma2dlem0i  15406  gausslemma2dlem1a  15407  2lgslem1c  15439  2sqlem10  15474  ex-ceil  15480  bj-nnbist  15498  bj-con1st  15505  bj-charfunbi  15565  bj-sucexg  15676  bj-om  15691  bj-inf2vnlem1  15724  trilpolemisumle  15795  cndcap  15816