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  5830  isoselem  5961  oprabid  6050  brabvv  6067  uchoice  6300  oprssdmm  6334  1stdm  6345  f1o2ndf1  6393  poxp  6397  rdgon  6552  frecfcllem  6570  nntri3or  6661  nntri1  6664  ensym  6955  en2  6998  xpen  7031  snnen2oprc  7046  phplem4on  7054  fict  7055  fidceq  7056  infiexmid  7066  php5fin  7071  fisbth  7072  fin0  7074  fin0or  7075  diffisn  7082  infnfi  7084  fidcen  7088  en2eqpr  7099  exmidpw  7100  exmidpweq  7101  pw1fin  7102  fientri3  7107  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  ssfidc  7130  relcnvfi  7140  fiuni  7177  eqinfti  7219  djulclb  7254  updjud  7281  omp1eomlem  7293  0ct  7306  ctmlemr  7307  ctssdclemn0  7309  ctssdccl  7310  enomnilem  7337  finomni  7339  exmidomni  7341  enmkvlem  7360  enwomnilem  7368  exmidontriimlem1  7436  onntri35  7455  onntri52  7462  dftap2  7470  exmidapne  7479  enq0sym  7652  enq0tr  7654  prarloclem3  7717  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemrl  7793  mulnqprlemru  7794  mulnqprlemfl  7795  mulnqprlemfu  7796  ltexprlemfl  7829  ltexprlemfu  7831  recexprlemopl  7845  recexprlemopu  7847  aptipr  7861  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  caucvgprlemladdfu  7897  caucvgprprlemexbt  7926  suplocexprlemrl  7937  suplocexprlemru  7939  suplocexprlemex  7942  srpospr  8003  elrealeu  8049  axarch  8111  axcaucvglemres  8119  nn0ge2m1nn  9462  elnn0z  9492  peano2z  9515  uzm1  9787  qapne  9873  rpregt0  9902  rpnegap  9921  xnn0dcle  10037  xnn0letri  10038  npnflt  10050  nmnfgt  10053  xaddf  10079  xaddval  10080  xltadd1  10111  xsubge0  10116  xleaddadd  10122  elfz1end  10290  1fv  10374  elfzonlteqm1  10456  qtri3or  10501  exbtwnzlemshrink  10509  rebtwn2zlemshrink  10514  ioom  10521  elicore  10527  modfzo0difsn  10658  modsumfzodifsn  10659  addmodlteq  10661  frecfzennn  10689  seq3f1olemstep  10777  ser0  10796  exp3vallem  10803  facp1  10993  faclbnd  11004  bcn1  11021  hashennnuni  11042  hashcl  11044  hashfz1  11046  hashen  11047  fihashdom  11067  hashun  11069  zfz1isolem1  11105  zfz1iso  11106  lencl  11121  sswrd  11126  swrdswrd  11290  swrdccatin2  11314  pfxccat3  11319  pfxccatpfx1  11321  sqrt0  11569  resqrexlemfp1  11574  cau3lem  11679  xrmaxifle  11811  xrmaxiflemval  11815  xrmaxltsup  11823  xrmaxadd  11826  climserle  11910  climcaucn  11916  iserabs  12041  isumshft  12056  cvgratgt0  12099  mertenslem2  12102  prodf1  12108  fprodunsn  12170  fprodfac  12181  eirrap  12344  bezoutlemzz  12578  dfgcd3  12586  nnmindc  12610  nnminle  12611  nninfctlemfo  12616  lcmcllem  12644  prmind2  12697  prm2orodd  12703  sqrt2irr0  12741  sqrt2irrap  12757  ennnfonelemjn  13028  ennnfonelemdm  13046  ennnfonelemim  13050  ctiunctlemfo  13065  isstructr  13102  basmex  13147  dfgrp2  13615  dfgrp3mlem  13686  mulgnngsum  13719  grpissubg  13786  ablsubsub23  13917  rrgmex  14281  lssmex  14375  lidlmex  14495  2idlmex  14521  df2idl2  14529  2idlss  14534  isbasis3g  14776  innei  14893  cnpnei  14949  cncnp2m  14961  cnptopresti  14968  cnptoprest2  14970  imasnopn  15029  xmettx  15240  cdivcncfap  15334  expcncf  15339  cnopnap  15341  ivthinclemdisj  15370  dvrecap  15443  dvmptfsum  15455  gausslemma2dlem0i  15792  gausslemma2dlem1a  15793  2lgslem1c  15825  2sqlem10  15860  lfgredg2dom  15989  ausgrusgrben  16025  ausgrumgrien  16027  ausgrusgrien  16028  uspgredg2vlem  16077  uspgredg2v  16078  usgredg2vlem2  16080  ushgredgedg  16083  ushgredgedgloop  16085  griedg0ssusgr  16108  vtxedgfi  16146  vtxlpfi  16147  wlk1walkdom  16216  wlk0prc  16229  clwwlknonex2  16296  eupthi  16306  ex-ceil  16344  bj-nnbist  16366  bj-con1st  16373  bj-charfunbi  16432  bj-sucexg  16543  bj-om  16558  bj-inf2vnlem1  16591  trilpolemisumle  16668  cndcap  16690  gfsumval  16707