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

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 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  272  simprbi  273  sylanb  282  sylan2b  285  anc2l  325  sylanblc  413  orbi2i  757  pm2.32  764  oranim  776  stabnot  828  exmiddc  831  pm2.1dc  832  stdcndcOLD  841  stdcn  842  const  847  imanst  883  pm5.75  957  rnlem  971  simp1bi  1007  simp2bi  1008  simp3bi  1009  syl3an1b  1269  syl3an2b  1270  syl3an3b  1271  exalim  1495  nford  1560  nfal  1569  stdpc5  1577  sbbii  1758  sb9i  1973  eu5  2066  exmoeudc  2082  eqeq1  2177  eleq2  2234  nner  2344  rexalim  2463  gencbvex  2776  gencbval  2778  moeq  2905  euind  2917  reuind  2935  ssel  3141  ssrmof  3210  unssd  3303  ssind  3351  unssdif  3362  ss0  3455  prprc  3693  disjnim  3980  trint  4102  snexprc  4172  undifexmid  4179  exmidn0m  4187  exmidsssn  4188  exmidundif  4192  exmidundifim  4193  pocl  4288  sotritrieq  4310  frirrg  4335  unexg  4428  abnex  4432  reusv3i  4444  ordtriexmid  4505  ontriexmidim  4506  ordtri2orexmid  4507  preleq  4539  0elsucexmid  4549  ordpwsucexmid  4554  ordtri2or2exmid  4555  elomssom  4589  brrelex12  4649  0nelrel  4657  elrel  4713  xpssres  4926  elres  4927  coi2  5127  iotabi  5169  uniabio  5170  nfunv  5231  funun  5242  funcnv3  5260  funimass1  5275  imain  5280  funssxp  5367  f0dom0  5391  f1o00  5477  fsn2  5670  isoselem  5799  oprabid  5885  brabvv  5899  oprssdmm  6150  1stdm  6161  f1o2ndf1  6207  poxp  6211  rdgon  6365  frecfcllem  6383  nntri3or  6472  nntri1  6475  ensym  6759  xpen  6823  snnen2oprc  6838  phplem4on  6845  fict  6846  fidceq  6847  infiexmid  6855  php5fin  6860  fisbth  6861  fin0  6863  fin0or  6864  diffisn  6871  infnfi  6873  en2eqpr  6885  exmidpw  6886  exmidpweq  6887  pw1fin  6888  fientri3  6892  unsnfi  6896  unsnfidcex  6897  unsnfidcel  6898  undifdcss  6900  ssfidc  6912  relcnvfi  6918  fiuni  6955  eqinfti  6997  djulclb  7032  updjud  7059  omp1eomlem  7071  0ct  7084  ctmlemr  7085  ctssdclemn0  7087  ctssdccl  7088  enomnilem  7114  finomni  7116  exmidomni  7118  enmkvlem  7137  enwomnilem  7145  exmidontriimlem1  7198  onntri35  7214  onntri52  7221  enq0sym  7394  enq0tr  7396  prarloclem3  7459  nqprl  7513  nqpru  7514  addnqprlemrl  7519  addnqprlemru  7520  addnqprlemfl  7521  addnqprlemfu  7522  mulnqprlemrl  7535  mulnqprlemru  7536  mulnqprlemfl  7537  mulnqprlemfu  7538  ltexprlemfl  7571  ltexprlemfu  7573  recexprlemopl  7587  recexprlemopu  7589  aptipr  7603  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  caucvgprlemladdfu  7639  caucvgprprlemexbt  7668  suplocexprlemrl  7679  suplocexprlemru  7681  suplocexprlemex  7684  srpospr  7745  elrealeu  7791  axarch  7853  axcaucvglemres  7861  nn0ge2m1nn  9195  elnn0z  9225  peano2z  9248  uzm1  9517  qapne  9598  rpregt0  9624  rpnegap  9643  xnn0dcle  9759  xnn0letri  9760  npnflt  9772  nmnfgt  9775  xaddf  9801  xaddval  9802  xltadd1  9833  xsubge0  9838  xleaddadd  9844  elfz1end  10011  1fv  10095  elfzonlteqm1  10166  qtri3or  10199  exbtwnzlemshrink  10205  rebtwn2zlemshrink  10210  ioom  10217  elicore  10223  modfzo0difsn  10351  modsumfzodifsn  10352  addmodlteq  10354  frecfzennn  10382  seq3f1olemstep  10457  ser0  10470  exp3vallem  10477  facp1  10664  faclbnd  10675  bcn1  10692  hashennnuni  10713  hashcl  10715  hashfz1  10717  hashen  10718  fihashdom  10738  hashun  10740  zfz1isolem1  10775  zfz1iso  10776  sqrt0  10968  resqrexlemfp1  10973  cau3lem  11078  xrmaxifle  11209  xrmaxiflemval  11213  xrmaxltsup  11221  xrmaxadd  11224  climserle  11308  climcaucn  11314  iserabs  11438  isumshft  11453  cvgratgt0  11496  mertenslem2  11499  prodf1  11505  fprodunsn  11567  fprodfac  11578  eirrap  11740  bezoutlemzz  11957  dfgcd3  11965  nnmindc  11989  nnminle  11990  lcmcllem  12021  prmind2  12074  prm2orodd  12080  sqrt2irr0  12118  sqrt2irrap  12134  ennnfonelemjn  12357  ennnfonelemdm  12375  ennnfonelemim  12379  ctiunctlemfo  12394  isstructr  12431  basmex  12474  dfgrp2  12732  isbasis3g  12838  innei  12957  cnpnei  13013  cncnp2m  13025  cnptopresti  13032  cnptoprest2  13034  imasnopn  13093  xmettx  13304  cdivcncfap  13381  expcncf  13386  cnopnap  13388  ivthinclemdisj  13412  dvrecap  13471  2sqlem10  13755  ex-ceil  13761  bj-nnbist  13779  bj-con1st  13786  bj-charfunbi  13846  bj-sucexg  13957  bj-om  13972  bj-inf2vnlem1  14005  exmid1stab  14033  trilpolemisumle  14070