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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used 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  birani  386  bilani  387  sylanblc  419  orbi2i  774  pm2.32  781  oranim  793  stabnot  845  exmiddc  848  pm2.1dc  849  stdcndcOLD  858  stdcn  859  const  864  imanst  900  pm5.75  975  rnlem  989  ifpnst  1001  simp1bi  1043  simp2bi  1044  simp3bi  1045  syl3an1b  1314  syl3an2b  1315  syl3an3b  1316  exalim  1555  nford  1620  nfal  1629  stdpc5  1637  sbbii  1818  sb9i  2040  eu5  2134  exmoeudc  2150  eqeq1  2245  eleq2  2302  nner  2424  rexalim  2543  gencbvex  2869  gencbval  2871  moeq  3001  euind  3013  reuind  3031  ssel  3242  ssrmof  3311  unssd  3405  ssind  3455  unssdif  3466  ss0  3563  rabsnif  3778  prprc  3823  disjnim  4120  trint  4246  snexprc  4325  undifexmid  4332  exmidn0m  4340  exmidsssn  4341  exmidundif  4345  exmidundifim  4346  exmid1stab  4347  pocl  4450  sotritrieq  4472  frirrg  4497  unexg  4591  abnex  4595  reusv3i  4607  ordtriexmid  4670  ontriexmidim  4671  ordtri2orexmid  4672  preleq  4704  0elsucexmid  4714  ordpwsucexmid  4719  ordtri2or2exmid  4720  elomssom  4754  brrelex12  4815  0nelrel  4823  elrel  4879  xpssres  5100  elres  5101  coi2  5307  iotabi  5350  uniabio  5351  nfunv  5413  funun  5425  funcnv3  5446  funimass1  5461  imain  5466  funssxp  5560  f0dom0  5589  f1o00  5679  fsn2  5885  funopsn  5894  isoselem  6029  oprabid  6120  brabvv  6137  uchoice  6375  oprssdmm  6409  1stdm  6420  f1o2ndf1  6468  poxp  6472  suppval1  6483  funsssuppss  6502  rdgon  6661  frecfcllem  6679  nntri3or  6770  nntri1  6773  ensym  7072  en2  7116  xpen  7149  snnen2oprc  7165  phplem4on  7173  fict  7174  fidceq  7175  infiexmid  7185  php5fin  7190  fisbth  7191  fin0  7193  fin0or  7194  diffisn  7201  infnfi  7203  fidcen  7207  en2eqpr  7218  exmidpw  7219  exmidpweq  7220  pw1fin  7221  fientri3  7226  unsnfi  7230  unsnfidcex  7231  unsnfidcel  7232  undifdcss  7234  ssfidc  7249  relcnvfi  7259  fiuni  7317  eqinfti  7366  djulclb  7401  updjud  7428  omp1eomlem  7440  0ct  7453  ctmlemr  7454  ctssdclemn0  7456  ctssdccl  7457  enomnilem  7484  finomni  7486  exmidomni  7488  enmkvlem  7507  enwomnilem  7515  exmidontriimlem1  7583  onntri35  7602  onntri52  7609  dftap2  7623  exmidapne  7632  enq0sym  7805  enq0tr  7807  prarloclem3  7870  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemrl  7946  mulnqprlemru  7947  mulnqprlemfl  7948  mulnqprlemfu  7949  ltexprlemfl  7982  ltexprlemfu  7984  recexprlemopl  7998  recexprlemopu  8000  aptipr  8014  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemladdfu  8050  caucvgprprlemexbt  8079  suplocexprlemrl  8090  suplocexprlemru  8092  suplocexprlemex  8095  srpospr  8156  elrealeu  8202  axarch  8264  axcaucvglemres  8272  nn0ge2m1nn  9638  elnn0z  9668  peano2z  9691  uzm1  9969  qapne  10055  rpregt0  10085  rpnegap  10104  xnn0dcle  10221  xnn0letri  10222  npnflt  10234  nmnfgt  10237  xaddf  10263  xaddval  10264  xltadd1  10295  xsubge0  10300  xleaddadd  10306  elfz1end  10478  1fv  10563  elfzonlteqm1  10645  qtri3or  10692  exbtwnzlemshrink  10700  rebtwn2zlemshrink  10705  ioom  10712  elicore  10718  modfzo0difsn  10853  modsumfzodifsn  10854  addmodlteq  10856  frecfzennn  10884  seq3f1olemstep  10972  ser0  10991  exp3vallem  10998  facp1  11190  faclbnd  11201  bcn1  11218  hashennnuni  11240  hashcl  11242  hashfz1  11244  hashen  11245  fihashdom  11265  hashun  11267  zfz1isolem1  11314  zfz1iso  11315  lencl  11330  sswrd  11335  swrdswrd  11499  swrdccatin2  11523  pfxccat3  11528  pfxccatpfx1  11530  sqrt0  11792  resqrexlemfp1  11797  cau3lem  11903  xrmaxifle  12037  xrmaxiflemval  12041  xrmaxltsup  12049  xrmaxadd  12052  climserle  12136  climcaucn  12142  iserabs  12267  isumshft  12282  cvgratgt0  12325  mertenslem2  12328  prodf1  12334  fprodunsn  12396  fprodfac  12407  eirrap  12570  bezoutlemzz  12804  dfgcd3  12812  nnmindc  12836  nnminle  12837  nninfctlemfo  12842  lcmcllem  12870  prmind2  12923  prm2orodd  12929  sqrt2irr0  12968  sqrt2irrap  12985  ballotfilem2  13286  ballotfilemic  13308  ballotfilem1c  13309  ennnfonelemjn  13351  ennnfonelemdm  13369  ennnfonelemim  13373  ctiunctlemfo  13388  isstructr  13425  basmex  13470  dfgrp2  13891  dfgrp3mlem  13962  mulgnngzsum  13989  grpissubg  14056  ablsubsub23  14219  gsumvalfi  14242  opprringb  14495  rrgmex  14678  aprprop  14710  lssmex  14801  lidlmex  14921  2idlmex  14947  df2idl2  14955  2idlss  14960  isbasis3g  15272  innei  15389  cnpnei  15445  cncnp2m  15457  cnptopresti  15464  cnptoprest2  15466  imasnopn  15525  xmettx  15736  cdivcncfap  15830  expcncf  15835  cnopnap  15837  ivthinclemdisj  15866  dvrecap  15939  dvmptfsum  15951  logfac  16126  prmorcht  16282  gausslemma2dlem0i  16381  gausslemma2dlem1a  16382  2lgslem1c  16414  2sqlem10  16449  lfgredg2dom  16578  ausgrusgrben  16614  ausgrumgrien  16616  ausgrusgrien  16617  uspgredg2vlem  16666  uspgredg2v  16667  usgredg2vlem2  16669  ushgredgedg  16672  ushgredgedgloop  16674  griedg0ssusgr  16697  vtxedgfi  16735  vtxlpfi  16736  wlk1walkdom  16805  wlk0prc  16818  clwwlknonex2  16885  eupthi  16895  ex-ceil  16945  bj-nnbist  16977  bj-con1st  16984  bj-charfunbi  17042  bj-sucexg  17153  bj-om  17168  bj-inf2vnlem1  17201  trilpolemisumle  17294  cndcap  17316  als-no-surprise  17354