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  770  pm2.32  777  oranim  789  stabnot  841  exmiddc  844  pm2.1dc  845  stdcndcOLD  854  stdcn  855  const  860  imanst  896  pm5.75  971  rnlem  985  ifpnst  997  simp1bi  1039  simp2bi  1040  simp3bi  1041  syl3an1b  1310  syl3an2b  1311  syl3an3b  1312  exalim  1551  nford  1616  nfal  1625  stdpc5  1633  sbbii  1814  sb9i  2036  eu5  2130  exmoeudc  2146  eqeq1  2241  eleq2  2298  nner  2418  rexalim  2537  gencbvex  2863  gencbval  2865  moeq  2995  euind  3007  reuind  3025  ssel  3236  ssrmof  3305  unssd  3399  ssind  3449  unssdif  3460  ss0  3553  rabsnif  3763  prprc  3807  disjnim  4104  trint  4228  snexprc  4304  undifexmid  4311  exmidn0m  4319  exmidsssn  4320  exmidundif  4324  exmidundifim  4325  exmid1stab  4326  pocl  4429  sotritrieq  4451  frirrg  4476  unexg  4569  abnex  4573  reusv3i  4585  ordtriexmid  4648  ontriexmidim  4649  ordtri2orexmid  4650  preleq  4682  0elsucexmid  4692  ordpwsucexmid  4697  ordtri2or2exmid  4698  elomssom  4732  brrelex12  4793  0nelrel  4801  elrel  4857  xpssres  5078  elres  5079  coi2  5284  iotabi  5327  uniabio  5328  nfunv  5390  funun  5402  funcnv3  5423  funimass1  5438  imain  5443  funssxp  5537  f0dom0  5566  f1o00  5656  fsn2  5856  funopsn  5865  isoselem  5999  oprabid  6090  brabvv  6107  uchoice  6344  oprssdmm  6378  1stdm  6389  f1o2ndf1  6437  poxp  6441  suppval1  6452  funsssuppss  6471  rdgon  6630  frecfcllem  6648  nntri3or  6739  nntri1  6742  ensym  7034  en2  7078  xpen  7111  snnen2oprc  7127  phplem4on  7135  fict  7136  fidceq  7137  infiexmid  7147  php5fin  7152  fisbth  7153  fin0  7155  fin0or  7156  diffisn  7163  infnfi  7165  fidcen  7169  en2eqpr  7180  exmidpw  7181  exmidpweq  7182  pw1fin  7183  fientri3  7188  unsnfi  7192  unsnfidcex  7193  unsnfidcel  7194  undifdcss  7196  ssfidc  7211  relcnvfi  7221  fiuni  7278  eqinfti  7324  djulclb  7359  updjud  7386  omp1eomlem  7398  0ct  7411  ctmlemr  7412  ctssdclemn0  7414  ctssdccl  7415  enomnilem  7442  finomni  7444  exmidomni  7446  enmkvlem  7465  enwomnilem  7473  exmidontriimlem1  7541  onntri35  7560  onntri52  7567  dftap2  7581  exmidapne  7590  enq0sym  7763  enq0tr  7765  prarloclem3  7828  nqprl  7882  nqpru  7883  addnqprlemrl  7888  addnqprlemru  7889  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemrl  7904  mulnqprlemru  7905  mulnqprlemfl  7906  mulnqprlemfu  7907  ltexprlemfl  7940  ltexprlemfu  7942  recexprlemopl  7956  recexprlemopu  7958  aptipr  7972  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  caucvgprlemladdfu  8008  caucvgprprlemexbt  8037  suplocexprlemrl  8048  suplocexprlemru  8050  suplocexprlemex  8053  srpospr  8114  elrealeu  8160  axarch  8222  axcaucvglemres  8230  nn0ge2m1nn  9577  elnn0z  9607  peano2z  9630  uzm1  9903  qapne  9989  rpregt0  10018  rpnegap  10037  xnn0dcle  10154  xnn0letri  10155  npnflt  10167  nmnfgt  10170  xaddf  10196  xaddval  10197  xltadd1  10228  xsubge0  10233  xleaddadd  10239  elfz1end  10410  1fv  10495  elfzonlteqm1  10577  qtri3or  10624  exbtwnzlemshrink  10632  rebtwn2zlemshrink  10637  ioom  10644  elicore  10650  modfzo0difsn  10781  modsumfzodifsn  10782  addmodlteq  10784  frecfzennn  10812  seq3f1olemstep  10900  ser0  10919  exp3vallem  10926  facp1  11117  faclbnd  11128  bcn1  11145  hashennnuni  11167  hashcl  11169  hashfz1  11171  hashen  11172  fihashdom  11192  hashun  11194  zfz1isolem1  11237  zfz1iso  11238  lencl  11253  sswrd  11258  swrdswrd  11422  swrdccatin2  11446  pfxccat3  11451  pfxccatpfx1  11453  sqrt0  11714  resqrexlemfp1  11719  cau3lem  11824  xrmaxifle  11956  xrmaxiflemval  11960  xrmaxltsup  11968  xrmaxadd  11971  climserle  12055  climcaucn  12061  iserabs  12186  isumshft  12201  cvgratgt0  12244  mertenslem2  12247  prodf1  12253  fprodunsn  12315  fprodfac  12326  eirrap  12489  bezoutlemzz  12723  dfgcd3  12731  nnmindc  12755  nnminle  12756  nninfctlemfo  12761  lcmcllem  12789  prmind2  12842  prm2orodd  12848  sqrt2irr0  12886  sqrt2irrap  12902  ballotfilem2  13172  ballotfilemic  13194  ballotfilem1c  13195  ennnfonelemjn  13237  ennnfonelemdm  13255  ennnfonelemim  13259  ctiunctlemfo  13274  isstructr  13311  basmex  13356  dfgrp2  13782  dfgrp3mlem  13853  mulgnngsum  13880  grpissubg  13947  ablsubsub23  14078  gfsumval  14102  opprringb  14324  rrgmex  14507  aprprop  14539  lssmex  14629  lidlmex  14749  2idlmex  14775  df2idl2  14783  2idlss  14788  isbasis3g  15037  innei  15154  cnpnei  15210  cncnp2m  15222  cnptopresti  15229  cnptoprest2  15231  imasnopn  15290  xmettx  15501  cdivcncfap  15595  expcncf  15600  cnopnap  15602  ivthinclemdisj  15631  dvrecap  15704  dvmptfsum  15716  gausslemma2dlem0i  16056  gausslemma2dlem1a  16057  2lgslem1c  16089  2sqlem10  16124  lfgredg2dom  16253  ausgrusgrben  16289  ausgrumgrien  16291  ausgrusgrien  16292  uspgredg2vlem  16341  uspgredg2v  16342  usgredg2vlem2  16344  ushgredgedg  16347  ushgredgedgloop  16349  griedg0ssusgr  16372  vtxedgfi  16410  vtxlpfi  16411  wlk1walkdom  16480  wlk0prc  16493  clwwlknonex2  16560  eupthi  16570  ex-ceil  16620  bj-nnbist  16642  bj-con1st  16649  bj-charfunbi  16707  bj-sucexg  16818  bj-om  16833  bj-inf2vnlem1  16866  trilpolemisumle  16948  cndcap  16970  trimul0or  16971