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  1813  sb9i  2033  eu5  2127  exmoeudc  2143  eqeq1  2238  eleq2  2295  nner  2407  rexalim  2526  gencbvex  2851  gencbval  2853  moeq  2982  euind  2994  reuind  3012  ssel  3222  ssrmof  3291  unssd  3385  ssind  3433  unssdif  3444  ss0  3537  rabsnif  3742  prprc  3786  disjnim  4083  trint  4207  snexprc  4282  undifexmid  4289  exmidn0m  4297  exmidsssn  4298  exmidundif  4302  exmidundifim  4303  exmid1stab  4304  pocl  4406  sotritrieq  4428  frirrg  4453  unexg  4546  abnex  4550  reusv3i  4562  ordtriexmid  4625  ontriexmidim  4626  ordtri2orexmid  4627  preleq  4659  0elsucexmid  4669  ordpwsucexmid  4674  ordtri2or2exmid  4675  elomssom  4709  brrelex12  4770  0nelrel  4778  elrel  4834  xpssres  5054  elres  5055  coi2  5260  iotabi  5303  uniabio  5304  nfunv  5366  funun  5378  funcnv3  5399  funimass1  5414  imain  5419  funssxp  5512  f0dom0  5539  f1o00  5629  fsn2  5829  funopsn  5838  isoselem  5971  oprabid  6060  brabvv  6077  uchoice  6309  oprssdmm  6343  1stdm  6354  f1o2ndf1  6402  poxp  6406  suppval1  6417  funsssuppss  6436  rdgon  6595  frecfcllem  6613  nntri3or  6704  nntri1  6707  ensym  6998  en2  7041  xpen  7074  snnen2oprc  7089  phplem4on  7097  fict  7098  fidceq  7099  infiexmid  7109  php5fin  7114  fisbth  7115  fin0  7117  fin0or  7118  diffisn  7125  infnfi  7127  fidcen  7131  en2eqpr  7142  exmidpw  7143  exmidpweq  7144  pw1fin  7145  fientri3  7150  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  undifdcss  7158  ssfidc  7173  relcnvfi  7183  fiuni  7220  eqinfti  7262  djulclb  7297  updjud  7324  omp1eomlem  7336  0ct  7349  ctmlemr  7350  ctssdclemn0  7352  ctssdccl  7353  enomnilem  7380  finomni  7382  exmidomni  7384  enmkvlem  7403  enwomnilem  7411  exmidontriimlem1  7479  onntri35  7498  onntri52  7505  dftap2  7513  exmidapne  7522  enq0sym  7695  enq0tr  7697  prarloclem3  7760  nqprl  7814  nqpru  7815  addnqprlemrl  7820  addnqprlemru  7821  addnqprlemfl  7822  addnqprlemfu  7823  mulnqprlemrl  7836  mulnqprlemru  7837  mulnqprlemfl  7838  mulnqprlemfu  7839  ltexprlemfl  7872  ltexprlemfu  7874  recexprlemopl  7888  recexprlemopu  7890  aptipr  7904  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  caucvgprlemladdfu  7940  caucvgprprlemexbt  7969  suplocexprlemrl  7980  suplocexprlemru  7982  suplocexprlemex  7985  srpospr  8046  elrealeu  8092  axarch  8154  axcaucvglemres  8162  nn0ge2m1nn  9506  elnn0z  9536  peano2z  9559  uzm1  9831  qapne  9917  rpregt0  9946  rpnegap  9965  xnn0dcle  10081  xnn0letri  10082  npnflt  10094  nmnfgt  10097  xaddf  10123  xaddval  10124  xltadd1  10155  xsubge0  10160  xleaddadd  10166  elfz1end  10335  1fv  10419  elfzonlteqm1  10501  qtri3or  10546  exbtwnzlemshrink  10554  rebtwn2zlemshrink  10559  ioom  10566  elicore  10572  modfzo0difsn  10703  modsumfzodifsn  10704  addmodlteq  10706  frecfzennn  10734  seq3f1olemstep  10822  ser0  10841  exp3vallem  10848  facp1  11038  faclbnd  11049  bcn1  11066  hashennnuni  11087  hashcl  11089  hashfz1  11091  hashen  11092  fihashdom  11112  hashun  11114  zfz1isolem1  11150  zfz1iso  11151  lencl  11166  sswrd  11171  swrdswrd  11335  swrdccatin2  11359  pfxccat3  11364  pfxccatpfx1  11366  sqrt0  11627  resqrexlemfp1  11632  cau3lem  11737  xrmaxifle  11869  xrmaxiflemval  11873  xrmaxltsup  11881  xrmaxadd  11884  climserle  11968  climcaucn  11974  iserabs  12099  isumshft  12114  cvgratgt0  12157  mertenslem2  12160  prodf1  12166  fprodunsn  12228  fprodfac  12239  eirrap  12402  bezoutlemzz  12636  dfgcd3  12644  nnmindc  12668  nnminle  12669  nninfctlemfo  12674  lcmcllem  12702  prmind2  12755  prm2orodd  12761  sqrt2irr0  12799  sqrt2irrap  12815  ennnfonelemjn  13086  ennnfonelemdm  13104  ennnfonelemim  13108  ctiunctlemfo  13123  isstructr  13160  basmex  13205  dfgrp2  13673  dfgrp3mlem  13744  mulgnngsum  13777  grpissubg  13844  ablsubsub23  13975  rrgmex  14339  lssmex  14434  lidlmex  14554  2idlmex  14580  df2idl2  14588  2idlss  14593  isbasis3g  14840  innei  14957  cnpnei  15013  cncnp2m  15025  cnptopresti  15032  cnptoprest2  15034  imasnopn  15093  xmettx  15304  cdivcncfap  15398  expcncf  15403  cnopnap  15405  ivthinclemdisj  15434  dvrecap  15507  dvmptfsum  15519  gausslemma2dlem0i  15859  gausslemma2dlem1a  15860  2lgslem1c  15892  2sqlem10  15927  lfgredg2dom  16056  ausgrusgrben  16092  ausgrumgrien  16094  ausgrusgrien  16095  uspgredg2vlem  16144  uspgredg2v  16145  usgredg2vlem2  16147  ushgredgedg  16150  ushgredgedgloop  16152  griedg0ssusgr  16175  vtxedgfi  16213  vtxlpfi  16214  wlk1walkdom  16283  wlk0prc  16296  clwwlknonex2  16363  eupthi  16373  ex-ceil  16423  bj-nnbist  16445  bj-con1st  16452  bj-charfunbi  16510  bj-sucexg  16621  bj-om  16636  bj-inf2vnlem1  16669  trilpolemisumle  16753  cndcap  16775  gfsumval  16792