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  769  pm2.32  776  oranim  788  stabnot  840  exmiddc  843  pm2.1dc  844  stdcndcOLD  853  stdcn  854  const  859  imanst  895  pm5.75  970  rnlem  984  ifpnst  996  simp1bi  1038  simp2bi  1039  simp3bi  1040  syl3an1b  1309  syl3an2b  1310  syl3an3b  1311  exalim  1550  nford  1615  nfal  1624  stdpc5  1632  sbbii  1813  sb9i  2033  eu5  2127  exmoeudc  2143  eqeq1  2238  eleq2  2295  nner  2406  rexalim  2525  gencbvex  2850  gencbval  2852  moeq  2981  euind  2993  reuind  3011  ssel  3221  ssrmof  3290  unssd  3383  ssind  3431  unssdif  3442  ss0  3535  rabsnif  3738  prprc  3782  disjnim  4078  trint  4202  snexprc  4276  undifexmid  4283  exmidn0m  4291  exmidsssn  4292  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  pocl  4400  sotritrieq  4422  frirrg  4447  unexg  4540  abnex  4544  reusv3i  4556  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  preleq  4653  0elsucexmid  4663  ordpwsucexmid  4668  ordtri2or2exmid  4669  elomssom  4703  brrelex12  4764  0nelrel  4772  elrel  4828  xpssres  5048  elres  5049  coi2  5253  iotabi  5296  uniabio  5297  nfunv  5359  funun  5371  funcnv3  5392  funimass1  5407  imain  5412  funssxp  5504  f0dom0  5530  f1o00  5620  fsn2  5821  funopsn  5829  isoselem  5960  oprabid  6049  brabvv  6066  uchoice  6299  oprssdmm  6333  1stdm  6344  f1o2ndf1  6392  poxp  6396  rdgon  6551  frecfcllem  6569  nntri3or  6660  nntri1  6663  ensym  6954  en2  6997  xpen  7030  snnen2oprc  7045  phplem4on  7053  fict  7054  fidceq  7055  infiexmid  7065  php5fin  7070  fisbth  7071  fin0  7073  fin0or  7074  diffisn  7081  infnfi  7083  fidcen  7087  en2eqpr  7098  exmidpw  7099  exmidpweq  7100  pw1fin  7101  fientri3  7106  unsnfi  7110  unsnfidcex  7111  unsnfidcel  7112  undifdcss  7114  ssfidc  7129  relcnvfi  7139  fiuni  7176  eqinfti  7218  djulclb  7253  updjud  7280  omp1eomlem  7292  0ct  7305  ctmlemr  7306  ctssdclemn0  7308  ctssdccl  7309  enomnilem  7336  finomni  7338  exmidomni  7340  enmkvlem  7359  enwomnilem  7367  exmidontriimlem1  7435  onntri35  7454  onntri52  7461  dftap2  7469  exmidapne  7478  enq0sym  7651  enq0tr  7653  prarloclem3  7716  nqprl  7770  nqpru  7771  addnqprlemrl  7776  addnqprlemru  7777  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprlemrl  7792  mulnqprlemru  7793  mulnqprlemfl  7794  mulnqprlemfu  7795  ltexprlemfl  7828  ltexprlemfu  7830  recexprlemopl  7844  recexprlemopu  7846  aptipr  7860  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  caucvgprlemladdfu  7896  caucvgprprlemexbt  7925  suplocexprlemrl  7936  suplocexprlemru  7938  suplocexprlemex  7941  srpospr  8002  elrealeu  8048  axarch  8110  axcaucvglemres  8118  nn0ge2m1nn  9461  elnn0z  9491  peano2z  9514  uzm1  9786  qapne  9872  rpregt0  9901  rpnegap  9920  xnn0dcle  10036  xnn0letri  10037  npnflt  10049  nmnfgt  10052  xaddf  10078  xaddval  10079  xltadd1  10110  xsubge0  10115  xleaddadd  10121  elfz1end  10289  1fv  10373  elfzonlteqm1  10454  qtri3or  10499  exbtwnzlemshrink  10507  rebtwn2zlemshrink  10512  ioom  10519  elicore  10525  modfzo0difsn  10656  modsumfzodifsn  10657  addmodlteq  10659  frecfzennn  10687  seq3f1olemstep  10775  ser0  10794  exp3vallem  10801  facp1  10991  faclbnd  11002  bcn1  11019  hashennnuni  11040  hashcl  11042  hashfz1  11044  hashen  11045  fihashdom  11065  hashun  11067  zfz1isolem1  11103  zfz1iso  11104  lencl  11116  sswrd  11121  swrdswrd  11285  swrdccatin2  11309  pfxccat3  11314  pfxccatpfx1  11316  sqrt0  11564  resqrexlemfp1  11569  cau3lem  11674  xrmaxifle  11806  xrmaxiflemval  11810  xrmaxltsup  11818  xrmaxadd  11821  climserle  11905  climcaucn  11911  iserabs  12035  isumshft  12050  cvgratgt0  12093  mertenslem2  12096  prodf1  12102  fprodunsn  12164  fprodfac  12175  eirrap  12338  bezoutlemzz  12572  dfgcd3  12580  nnmindc  12604  nnminle  12605  nninfctlemfo  12610  lcmcllem  12638  prmind2  12691  prm2orodd  12697  sqrt2irr0  12735  sqrt2irrap  12751  ennnfonelemjn  13022  ennnfonelemdm  13040  ennnfonelemim  13044  ctiunctlemfo  13059  isstructr  13096  basmex  13141  dfgrp2  13609  dfgrp3mlem  13680  mulgnngsum  13713  grpissubg  13780  ablsubsub23  13911  rrgmex  14274  lssmex  14368  lidlmex  14488  2idlmex  14514  df2idl2  14522  2idlss  14527  isbasis3g  14769  innei  14886  cnpnei  14942  cncnp2m  14954  cnptopresti  14961  cnptoprest2  14963  imasnopn  15022  xmettx  15233  cdivcncfap  15327  expcncf  15332  cnopnap  15334  ivthinclemdisj  15363  dvrecap  15436  dvmptfsum  15448  gausslemma2dlem0i  15785  gausslemma2dlem1a  15786  2lgslem1c  15818  2sqlem10  15853  lfgredg2dom  15982  ausgrusgrben  16018  ausgrumgrien  16020  ausgrusgrien  16021  uspgredg2vlem  16070  uspgredg2v  16071  usgredg2vlem2  16073  ushgredgedg  16076  ushgredgedgloop  16078  griedg0ssusgr  16101  vtxedgfi  16139  vtxlpfi  16140  wlk1walkdom  16209  wlk0prc  16222  clwwlknonex2  16289  eupthi  16299  ex-ceil  16322  bj-nnbist  16340  bj-con1st  16347  bj-charfunbi  16406  bj-sucexg  16517  bj-om  16532  bj-inf2vnlem1  16565  trilpolemisumle  16642  cndcap  16663  gfsumval  16680