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  763  pm2.32  770  oranim  782  stabnot  834  exmiddc  837  pm2.1dc  838  stdcndcOLD  847  stdcn  848  const  853  imanst  889  pm5.75  964  rnlem  978  simp1bi  1014  simp2bi  1015  simp3bi  1016  syl3an1b  1285  syl3an2b  1286  syl3an3b  1287  exalim  1513  nford  1578  nfal  1587  stdpc5  1595  sbbii  1776  sb9i  1996  eu5  2089  exmoeudc  2105  eqeq1  2200  eleq2  2257  nner  2368  rexalim  2487  gencbvex  2806  gencbval  2808  moeq  2935  euind  2947  reuind  2965  ssel  3173  ssrmof  3242  unssd  3335  ssind  3383  unssdif  3394  ss0  3487  prprc  3728  disjnim  4020  trint  4142  snexprc  4215  undifexmid  4222  exmidn0m  4230  exmidsssn  4231  exmidundif  4235  exmidundifim  4236  exmid1stab  4237  pocl  4334  sotritrieq  4356  frirrg  4381  unexg  4474  abnex  4478  reusv3i  4490  ordtriexmid  4553  ontriexmidim  4554  ordtri2orexmid  4555  preleq  4587  0elsucexmid  4597  ordpwsucexmid  4602  ordtri2or2exmid  4603  elomssom  4637  brrelex12  4697  0nelrel  4705  elrel  4761  xpssres  4977  elres  4978  coi2  5182  iotabi  5224  uniabio  5225  nfunv  5287  funun  5298  funcnv3  5316  funimass1  5331  imain  5336  funssxp  5423  f0dom0  5447  f1o00  5535  fsn2  5732  isoselem  5863  oprabid  5950  brabvv  5964  uchoice  6190  oprssdmm  6224  1stdm  6235  f1o2ndf1  6281  poxp  6285  rdgon  6439  frecfcllem  6457  nntri3or  6546  nntri1  6549  ensym  6835  xpen  6901  snnen2oprc  6916  phplem4on  6923  fict  6924  fidceq  6925  infiexmid  6933  php5fin  6938  fisbth  6939  fin0  6941  fin0or  6942  diffisn  6949  infnfi  6951  en2eqpr  6963  exmidpw  6964  exmidpweq  6965  pw1fin  6966  fientri3  6971  unsnfi  6975  unsnfidcex  6976  unsnfidcel  6977  undifdcss  6979  ssfidc  6991  relcnvfi  7000  fiuni  7037  eqinfti  7079  djulclb  7114  updjud  7141  omp1eomlem  7153  0ct  7166  ctmlemr  7167  ctssdclemn0  7169  ctssdccl  7170  enomnilem  7197  finomni  7199  exmidomni  7201  enmkvlem  7220  enwomnilem  7228  exmidontriimlem1  7281  onntri35  7297  onntri52  7304  dftap2  7311  exmidapne  7320  enq0sym  7492  enq0tr  7494  prarloclem3  7557  nqprl  7611  nqpru  7612  addnqprlemrl  7617  addnqprlemru  7618  addnqprlemfl  7619  addnqprlemfu  7620  mulnqprlemrl  7633  mulnqprlemru  7634  mulnqprlemfl  7635  mulnqprlemfu  7636  ltexprlemfl  7669  ltexprlemfu  7671  recexprlemopl  7685  recexprlemopu  7687  aptipr  7701  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  caucvgprlemladdfu  7737  caucvgprprlemexbt  7766  suplocexprlemrl  7777  suplocexprlemru  7779  suplocexprlemex  7782  srpospr  7843  elrealeu  7889  axarch  7951  axcaucvglemres  7959  nn0ge2m1nn  9300  elnn0z  9330  peano2z  9353  uzm1  9623  qapne  9704  rpregt0  9733  rpnegap  9752  xnn0dcle  9868  xnn0letri  9869  npnflt  9881  nmnfgt  9884  xaddf  9910  xaddval  9911  xltadd1  9942  xsubge0  9947  xleaddadd  9953  elfz1end  10121  1fv  10205  elfzonlteqm1  10277  qtri3or  10310  exbtwnzlemshrink  10317  rebtwn2zlemshrink  10322  ioom  10329  elicore  10335  modfzo0difsn  10466  modsumfzodifsn  10467  addmodlteq  10469  frecfzennn  10497  seq3f1olemstep  10585  ser0  10604  exp3vallem  10611  facp1  10801  faclbnd  10812  bcn1  10829  hashennnuni  10850  hashcl  10852  hashfz1  10854  hashen  10855  fihashdom  10874  hashun  10876  zfz1isolem1  10911  zfz1iso  10912  lencl  10918  sswrd  10923  sqrt0  11148  resqrexlemfp1  11153  cau3lem  11258  xrmaxifle  11389  xrmaxiflemval  11393  xrmaxltsup  11401  xrmaxadd  11404  climserle  11488  climcaucn  11494  iserabs  11618  isumshft  11633  cvgratgt0  11676  mertenslem2  11679  prodf1  11685  fprodunsn  11747  fprodfac  11758  eirrap  11921  bezoutlemzz  12139  dfgcd3  12147  nnmindc  12171  nnminle  12172  nninfctlemfo  12177  lcmcllem  12205  prmind2  12258  prm2orodd  12264  sqrt2irr0  12302  sqrt2irrap  12318  ennnfonelemjn  12559  ennnfonelemdm  12577  ennnfonelemim  12581  ctiunctlemfo  12596  isstructr  12633  basmex  12677  dfgrp2  13099  dfgrp3mlem  13170  mulgnngsum  13197  grpissubg  13264  ablsubsub23  13395  rrgmex  13757  lssmex  13851  lidlmex  13971  2idlmex  13997  df2idl2  14005  2idlss  14010  isbasis3g  14214  innei  14331  cnpnei  14387  cncnp2m  14399  cnptopresti  14406  cnptoprest2  14408  imasnopn  14467  xmettx  14678  cdivcncfap  14758  expcncf  14763  cnopnap  14765  ivthinclemdisj  14794  dvrecap  14862  gausslemma2dlem0i  15173  gausslemma2dlem1a  15174  2sqlem10  15212  ex-ceil  15218  bj-nnbist  15236  bj-con1st  15243  bj-charfunbi  15303  bj-sucexg  15414  bj-om  15429  bj-inf2vnlem1  15462  trilpolemisumle  15528  cndcap  15549