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  7361  djulclb  7396  updjud  7423  omp1eomlem  7435  0ct  7448  ctmlemr  7449  ctssdclemn0  7451  ctssdccl  7452  enomnilem  7479  finomni  7481  exmidomni  7483  enmkvlem  7502  enwomnilem  7510  exmidontriimlem1  7578  onntri35  7597  onntri52  7604  dftap2  7618  exmidapne  7627  enq0sym  7800  enq0tr  7802  prarloclem3  7865  nqprl  7919  nqpru  7920  addnqprlemrl  7925  addnqprlemru  7926  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemrl  7941  mulnqprlemru  7942  mulnqprlemfl  7943  mulnqprlemfu  7944  ltexprlemfl  7977  ltexprlemfu  7979  recexprlemopl  7993  recexprlemopu  7995  aptipr  8009  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  caucvgprlemladdfu  8045  caucvgprprlemexbt  8074  suplocexprlemrl  8085  suplocexprlemru  8087  suplocexprlemex  8090  srpospr  8151  elrealeu  8197  axarch  8259  axcaucvglemres  8267  nn0ge2m1nn  9632  elnn0z  9662  peano2z  9685  uzm1  9963  qapne  10049  rpregt0  10079  rpnegap  10098  xnn0dcle  10215  xnn0letri  10216  npnflt  10228  nmnfgt  10231  xaddf  10257  xaddval  10258  xltadd1  10289  xsubge0  10294  xleaddadd  10300  elfz1end  10472  1fv  10557  elfzonlteqm1  10639  qtri3or  10686  exbtwnzlemshrink  10694  rebtwn2zlemshrink  10699  ioom  10706  elicore  10712  modfzo0difsn  10847  modsumfzodifsn  10848  addmodlteq  10850  frecfzennn  10878  seq3f1olemstep  10966  ser0  10985  exp3vallem  10992  facp1  11184  faclbnd  11195  bcn1  11212  hashennnuni  11234  hashcl  11236  hashfz1  11238  hashen  11239  fihashdom  11259  hashun  11261  zfz1isolem1  11308  zfz1iso  11309  lencl  11324  sswrd  11329  swrdswrd  11493  swrdccatin2  11517  pfxccat3  11522  pfxccatpfx1  11524  sqrt0  11786  resqrexlemfp1  11791  cau3lem  11897  xrmaxifle  12031  xrmaxiflemval  12035  xrmaxltsup  12043  xrmaxadd  12046  climserle  12130  climcaucn  12136  iserabs  12261  isumshft  12276  cvgratgt0  12319  mertenslem2  12322  prodf1  12328  fprodunsn  12390  fprodfac  12401  eirrap  12564  bezoutlemzz  12798  dfgcd3  12806  nnmindc  12830  nnminle  12831  nninfctlemfo  12836  lcmcllem  12864  prmind2  12917  prm2orodd  12923  sqrt2irr0  12962  sqrt2irrap  12979  ballotfilem2  13280  ballotfilemic  13302  ballotfilem1c  13303  ennnfonelemjn  13345  ennnfonelemdm  13363  ennnfonelemim  13367  ctiunctlemfo  13382  isstructr  13419  basmex  13464  dfgrp2  13885  dfgrp3mlem  13956  mulgnngzsum  13983  grpissubg  14050  ablsubsub23  14213  gsumvalfi  14236  opprringb  14470  rrgmex  14653  aprprop  14685  lssmex  14776  lidlmex  14896  2idlmex  14922  df2idl2  14930  2idlss  14935  isbasis3g  15238  innei  15355  cnpnei  15411  cncnp2m  15423  cnptopresti  15430  cnptoprest2  15432  imasnopn  15491  xmettx  15702  cdivcncfap  15796  expcncf  15801  cnopnap  15803  ivthinclemdisj  15832  dvrecap  15905  dvmptfsum  15917  logfac  16090  prmorcht  16243  gausslemma2dlem0i  16342  gausslemma2dlem1a  16343  2lgslem1c  16375  2sqlem10  16410  lfgredg2dom  16539  ausgrusgrben  16575  ausgrumgrien  16577  ausgrusgrien  16578  uspgredg2vlem  16627  uspgredg2v  16628  usgredg2vlem2  16630  ushgredgedg  16633  ushgredgedgloop  16635  griedg0ssusgr  16658  vtxedgfi  16696  vtxlpfi  16697  wlk1walkdom  16766  wlk0prc  16779  clwwlknonex2  16846  eupthi  16856  ex-ceil  16906  bj-nnbist  16938  bj-con1st  16945  bj-charfunbi  17003  bj-sucexg  17114  bj-om  17129  bj-inf2vnlem1  17162  trilpolemisumle  17254  cndcap  17276  als-no-surprise  17314