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  4244  snexprc  4323  undifexmid  4330  exmidn0m  4338  exmidsssn  4339  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  pocl  4448  sotritrieq  4470  frirrg  4495  unexg  4589  abnex  4593  reusv3i  4605  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  preleq  4702  0elsucexmid  4712  ordpwsucexmid  4717  ordtri2or2exmid  4718  elomssom  4752  brrelex12  4813  0nelrel  4821  elrel  4877  xpssres  5098  elres  5099  coi2  5304  iotabi  5347  uniabio  5348  nfunv  5410  funun  5422  funcnv3  5443  funimass1  5458  imain  5463  funssxp  5557  f0dom0  5586  f1o00  5676  fsn2  5882  funopsn  5891  isoselem  6026  oprabid  6117  brabvv  6134  uchoice  6371  oprssdmm  6405  1stdm  6416  f1o2ndf1  6464  poxp  6468  suppval1  6479  funsssuppss  6498  rdgon  6657  frecfcllem  6675  nntri3or  6766  nntri1  6769  ensym  7068  en2  7112  xpen  7145  snnen2oprc  7161  phplem4on  7169  fict  7170  fidceq  7171  infiexmid  7181  php5fin  7186  fisbth  7187  fin0  7189  fin0or  7190  diffisn  7197  infnfi  7199  fidcen  7203  en2eqpr  7214  exmidpw  7215  exmidpweq  7216  pw1fin  7217  fientri3  7222  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  ssfidc  7245  relcnvfi  7255  fiuni  7312  eqinfti  7360  djulclb  7395  updjud  7422  omp1eomlem  7434  0ct  7447  ctmlemr  7448  ctssdclemn0  7450  ctssdccl  7451  enomnilem  7478  finomni  7480  exmidomni  7482  enmkvlem  7501  enwomnilem  7509  exmidontriimlem1  7577  onntri35  7596  onntri52  7603  dftap2  7617  exmidapne  7626  enq0sym  7799  enq0tr  7801  prarloclem3  7864  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemrl  7940  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  ltexprlemfl  7976  ltexprlemfu  7978  recexprlemopl  7992  recexprlemopu  7994  aptipr  8008  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemladdfu  8044  caucvgprprlemexbt  8073  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemex  8089  srpospr  8150  elrealeu  8196  axarch  8258  axcaucvglemres  8266  nn0ge2m1nn  9627  elnn0z  9657  peano2z  9680  uzm1  9953  qapne  10039  rpregt0  10068  rpnegap  10087  xnn0dcle  10204  xnn0letri  10205  npnflt  10217  nmnfgt  10220  xaddf  10246  xaddval  10247  xltadd1  10278  xsubge0  10283  xleaddadd  10289  elfz1end  10461  1fv  10546  elfzonlteqm1  10628  qtri3or  10675  exbtwnzlemshrink  10683  rebtwn2zlemshrink  10688  ioom  10695  elicore  10701  modfzo0difsn  10832  modsumfzodifsn  10833  addmodlteq  10835  frecfzennn  10863  seq3f1olemstep  10951  ser0  10970  exp3vallem  10977  facp1  11168  faclbnd  11179  bcn1  11196  hashennnuni  11218  hashcl  11220  hashfz1  11222  hashen  11223  fihashdom  11243  hashun  11245  zfz1isolem1  11292  zfz1iso  11293  lencl  11308  sswrd  11313  swrdswrd  11477  swrdccatin2  11501  pfxccat3  11506  pfxccatpfx1  11508  sqrt0  11770  resqrexlemfp1  11775  cau3lem  11880  xrmaxifle  12012  xrmaxiflemval  12016  xrmaxltsup  12024  xrmaxadd  12027  climserle  12111  climcaucn  12117  iserabs  12242  isumshft  12257  cvgratgt0  12300  mertenslem2  12303  prodf1  12309  fprodunsn  12371  fprodfac  12382  eirrap  12545  bezoutlemzz  12779  dfgcd3  12787  nnmindc  12811  nnminle  12812  nninfctlemfo  12817  lcmcllem  12845  prmind2  12898  prm2orodd  12904  sqrt2irr0  12942  sqrt2irrap  12958  ballotfilem2  13228  ballotfilemic  13250  ballotfilem1c  13251  ennnfonelemjn  13293  ennnfonelemdm  13311  ennnfonelemim  13315  ctiunctlemfo  13330  isstructr  13367  basmex  13412  dfgrp2  13832  dfgrp3mlem  13903  mulgnngzsum  13930  grpissubg  13997  ablsubsub23  14129  gsumvalfi  14152  opprringb  14386  rrgmex  14569  aprprop  14601  lssmex  14692  lidlmex  14812  2idlmex  14838  df2idl2  14846  2idlss  14851  isbasis3g  15147  innei  15264  cnpnei  15320  cncnp2m  15332  cnptopresti  15339  cnptoprest2  15341  imasnopn  15400  xmettx  15611  cdivcncfap  15705  expcncf  15710  cnopnap  15712  ivthinclemdisj  15741  dvrecap  15814  dvmptfsum  15826  logfac  15995  gausslemma2dlem0i  16176  gausslemma2dlem1a  16177  2lgslem1c  16209  2sqlem10  16244  lfgredg2dom  16373  ausgrusgrben  16409  ausgrumgrien  16411  ausgrusgrien  16412  uspgredg2vlem  16461  uspgredg2v  16462  usgredg2vlem2  16464  ushgredgedg  16467  ushgredgedgloop  16469  griedg0ssusgr  16492  vtxedgfi  16530  vtxlpfi  16531  wlk1walkdom  16600  wlk0prc  16613  clwwlknonex2  16680  eupthi  16690  ex-ceil  16740  bj-nnbist  16772  bj-con1st  16779  bj-charfunbi  16837  bj-sucexg  16948  bj-om  16963  bj-inf2vnlem1  16996  trilpolemisumle  17087  cndcap  17109  als-no-surprise  17147