Theorem mpd 13

Description: A modus ponens deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpd.1	⊢ (𝜑 → 𝜓)
mpd.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mpd	⊢ (𝜑 → 𝜒)

Proof of Theorem mpd

Step	Hyp	Ref	Expression
1		mpd.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpd.2	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	a2i 11	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
4	1, 3	ax-mp 5	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-2 7

This theorem is referenced by:  syl  14  mpi  15  id  19  mpcom  36  mpdd  41  mp2d  47  pm2.43i  49  syl3c  63  mpbid  147  mpbird  167  jcai  311  mp2and  433  pm2.21dd  623  mt2d  628  mpnanrd  697  mpjaod  723  stdcndcOLD  851  impidc  863  jadc  868  pm2.54dc  896  oplem1  981  mp3and  1374  xor3dc  1429  exlimdd  1918  exlimddv  1945  eqrdav  2228  necon1aidc  2451  necon1bidc  2452  necon4aidc  2468  reximddv  2633  reximssdv  2634  rexlimddv  2653  vtoclgft  2851  rspcedvd  2913  sseldd  3225  ssneldd  3227  tpid3g  3782  preq12b  3848  axpweq  4256  exmid1dc  4285  exmid1stab  4293  opth  4324  issod  4411  frirrg  4442  frind  4444  ralxfr2d  4556  rexxfr2d  4557  eldifpw  4569  onun2  4583  onuni  4587  elirr  4634  en2lp  4647  wetriext  4670  peano2  4688  relop  4875  elres  5044  sotri2  5129  iota4an  5302  iota5  5303  funeu  5346  funopg  5355  imadiflem  5403  funimaexglem  5407  ssimaex  5700  ffvelcdm  5773  dff3im  5785  dffo4  5788  funopsn  5822  f1eqcocnv  5924  f1oiso2  5960  riota5f  5990  riotass2  5992  acexmidlemcase  6005  elovimad  6054  ovmpodf  6145  ovmpodv2  6147  ovi3  6151  ov6g  6152  caoftrn  6260  op1steq  6334  tfr0dm  6479  tfrlemibxssdm  6484  tfrlemi14d  6490  tfr1onlembxssdm  6500  tfr1onlemaccex  6505  tfr1onlemres  6506  tfrcllembxssdm  6513  tfrcllemaccex  6518  tfrcllemres  6519  rdgivallem  6538  nnsucelsuc  6650  nnsucsssuc  6651  dcdifsnid  6663  nnawordex  6688  ersym  6705  mapvalg  6818  pmvalg  6819  mapsn  6850  fundmen  6972  en2  6986  pw2f1odclem  7008  mapdom1g  7021  fidceq  7044  fin0or  7061  findcard2  7064  findcard2s  7065  fidcen  7074  prfidceq  7106  fiintim  7109  suplub2ti  7184  supsnti  7188  supisoex  7192  difinfsnlem  7282  difinfsn  7283  ctm  7292  ctssdclemn0  7293  ctssdccl  7294  ctssdc  7296  enumctlemm  7297  nninfninc  7306  nnnninfeq2  7312  enomnilem  7321  exmidomniim  7324  exmidomni  7325  fodjuomnilemdc  7327  fodjuomnilemres  7331  omnimkv  7339  mkvprop  7341  omniwomnimkv  7350  en2prde  7382  pr2cv1  7384  en2eleq  7389  acfun  7405  exmidontriimlem1  7419  exmidontriimlem4  7422  exmidontriim  7423  ccfunen  7466  cc4f  7471  cc4n  7473  elni2  7517  mulclpi  7531  nlt1pig  7544  indpi  7545  recclnq  7595  ltexnqq  7611  halfnqq  7613  prarloclemarch  7621  prarloclemarch2  7622  prop  7678  prltlu  7690  prarloclem3step  7699  prarloclem5  7703  prarloclem  7704  prarloc  7706  prarloc2  7707  genpml  7720  genpmu  7721  genprndl  7724  genprndu  7725  genpdisj  7726  addnqprllem  7730  addnqprulem  7731  addlocprlemeq  7736  addlocprlemgt  7737  addlocprlem  7738  addlocpr  7739  nqprloc  7748  nqprl  7754  nqpru  7755  addnqprlemrl  7760  addnqprlemru  7761  appdivnq  7766  prmuloc  7769  prmuloc2  7770  mullocprlem  7773  mullocpr  7774  mulnqprlemrl  7776  mulnqprlemru  7777  ltprordil  7792  ltpopr  7798  ltsopr  7799  ltaddpr  7800  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemlol  7805  ltexprlemopu  7806  ltexprlemupu  7807  ltexprlemloc  7810  ltexprlemfl  7812  ltexprlemrl  7813  ltexprlemfu  7814  ltexprlemru  7815  ltaprg  7822  recexprlemm  7827  recexprlem1ssl  7836  recexprlem1ssu  7837  aptiprleml  7842  aptiprlemu  7843  archpr  7846  cauappcvgprlemm  7848  cauappcvgprlemopl  7849  cauappcvgprlemlol  7850  cauappcvgprlemopu  7851  cauappcvgprlemupu  7852  cauappcvgprlemdisj  7854  cauappcvgprlemloc  7855  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  cauappcvgprlemladdru  7859  cauappcvgprlem1  7862  archrecpr  7867  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemm  7871  caucvgprlemopl  7872  caucvgprlemlol  7873  caucvgprlemopu  7874  caucvgprlemupu  7875  caucvgprlemdisj  7877  caucvgprlemloc  7878  caucvgprlemladdfu  7880  caucvgprlem1  7882  caucvgprlemlim  7884  caucvgprprlemnbj  7896  caucvgprprlemml  7897  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemopu  7902  caucvgprprlemupu  7903  caucvgprprlemdisj  7905  caucvgprprlemloc  7906  caucvgprprlemexbt  7909  caucvgprprlemaddq  7911  caucvgprprlemlim  7914  suplocexprlemss  7918  suplocexprlemrl  7920  suplocexprlemmu  7921  suplocexprlemru  7922  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemub  7926  suplocexprlemlub  7927  recexgt0sr  7976  mulgt0sr  7981  archsr  7985  caucvgsrlemoffcau  8001  suplocsrlemb  8009  suplocsrlempr  8010  suplocsrlem  8011  cnm  8035  axarch  8094  axcaucvglemcau  8101  axpre-suploclemres  8104  lelttr  8251  ltletr  8252  ltled  8281  cnegexlem1  8337  cnegexlem2  8338  renegcl  8423  negf1o  8544  gt0add  8736  apreap  8750  apirr  8768  apsym  8769  apcotr  8770  apadd1  8771  apneg  8774  mulext1  8775  mulap0r  8778  apti  8785  aprcl  8809  aptap  8813  recexap  8816  mulap0  8817  receuap  8832  mul0eqap  8833  lep1  9008  lem1  9010  letrp1  9011  recreclt  9063  lbinf  9111  suprubex  9114  nnrecgt0  9164  bndndx  9384  nn0ge2m1nn  9445  elnn0z  9475  peano2z  9498  zaddcl  9502  ztri3or0  9504  zltnle  9508  zdceq  9538  zdcle  9539  zdclt  9540  zdiv  9551  zeo  9568  fnn0ind  9579  btwnz  9582  uzm1  9770  uzp1  9773  indstr  9805  supinfneg  9807  infsupneg  9808  eluzdc  9822  nn01to3  9829  qapne  9851  xrltled  10012  xrlelttr  10019  xrltletr  10020  ge0nemnf  10037  fzdcel  10253  elfzouz2  10375  fzoss1  10386  fzospliti  10391  elincfzoext  10416  fzocatel  10422  fzostep1  10460  zsupcllemstep  10466  zsupcl  10468  infssuzledc  10471  qtri3or  10477  qltnle  10480  qdceq  10481  qdclt  10482  exbtwnzlemex  10486  rebtwn2zlemstep  10489  rebtwn2z  10491  qbtwnxr  10494  ioom  10497  ico0  10498  ioc0  10499  flqeqceilz  10557  modqadd1  10600  modqmul1  10616  frec2uzuzd  10641  frec2uzlt2d  10643  frec2uzf1od  10645  frecuzrdgrrn  10647  frec2uzrdg  10648  frecuzrdgrcl  10649  frecuzrdgsuc  10653  frecuzrdgrclt  10654  frecuzrdgdomlem  10656  uzsinds  10683  seqvalcd  10700  seqovcd  10706  seq3fveq2  10714  seqfveq2g  10716  seq3shft2  10720  seqshft2g  10721  monoord  10724  seq3split  10727  seqsplitg  10728  seq3caopr3  10730  iseqf1olemab  10741  iseqf1olemnanb  10742  iseqf1olemqk  10746  seqf1oglem1  10758  seqf1og  10760  seq3id3  10763  seq3id2  10765  seq3homo  10766  seqhomog  10769  expgt1  10816  m1expeven  10825  expnbnd  10902  expnlbnd2  10904  nn0ltexp2  10948  apexp1  10957  hashennn  11019  zfz1isolem1  11080  seq3coll  11082  pfxwrdsymbg  11243  wrdind  11275  wrd2ind  11276  cjap  11438  caucvgre  11513  cvg1nlemres  11517  resqrexlemgt0  11552  resqrexlemglsq  11554  resqrexlemga  11555  resqrtcl  11561  abslt  11620  abssubap0  11622  abssubne0  11623  caubnd2  11649  qdenre  11734  maxabslemlub  11739  maxabs  11741  maxleast  11745  fimaxre2  11759  xrmaxiflemlub  11780  xrmaxif  11783  xrmaxltsup  11790  xrmaxadd  11793  xrmineqinf  11801  climuni  11825  2clim  11833  climcn1  11840  climcn2  11841  subcn2  11843  mulcn2  11844  climsqz  11867  climsqz2  11868  climcau  11879  climcvg1nlem  11881  climcaucn  11883  serf0  11884  sumrbdclem  11909  summodclem2  11914  zsumdc  11916  divcnv  12029  absltap  12041  absgtap  12042  mertenslem2  12068  ntrivcvgap  12080  prodrbdclem  12103  prodmodclem2  12109  zproddc  12111  prodssdc  12121  fprodsplitdc  12128  fprodcl2lem  12137  efcllemp  12190  tanvalap  12240  sin01bnd  12289  cos01bnd  12290  sin01gt0  12294  absef  12302  eirrap  12310  dvds0  12338  dvdsmul1  12345  dvdsmultr1d  12364  dvdslelemd  12375  divconjdvds  12381  alzdvds  12386  3dvds  12396  sqoddm1div8z  12418  nno  12438  divalglemex  12454  bits0o  12482  dvdsbnd  12498  dvdslegcd  12506  zeqzmulgcd  12512  gcd0id  12521  gcdaddm  12526  gcd1  12529  gcdabs  12530  bezoutlemnewy  12538  bezoutlemstep  12539  bezoutlemmain  12540  bezoutlemex  12543  bezoutlemzz  12544  bezoutlemaz  12545  bezoutlembz  12546  bezoutlembi  12547  bezoutlemle  12550  bezoutlemsup  12551  mulgcd  12558  gcdzeq  12564  dvdsmulgcd  12567  sqgcd  12571  bezoutr1  12575  nninfctlemfo  12582  algcvga  12594  algfx  12595  eucalglt  12600  eucalg  12602  lcmneg  12617  lcmabs  12619  lcmgcdlem  12620  ncoprmgcdne1b  12632  mulgcddvds  12637  qredeq  12639  divgcdcoprm0  12644  cncongr1  12646  isprm2lem  12659  nprm  12666  dvdsnprmd  12668  prmdvdsfz  12682  isprm5lem  12684  coprm  12687  isprm6  12690  sqrt2irr  12705  pw2dvdslemn  12708  pw2dvdseulemle  12710  oddpwdclemdvds  12713  oddpwdclemndvds  12714  sqrt2irrap  12723  qnumdencl  12730  prmdiv  12778  modprmn0modprm0  12800  prm23lt5  12807  pythagtriplem4  12812  pythagtriplem19  12826  pythagtrip  12827  pclemub  12831  pcpre1  12836  pcpremul  12837  pceulem  12838  pcqcl  12850  pcidlem  12867  pcgcd1  12872  pc2dvds  12874  dvdsprmpweqle  12881  difsqpwdvds  12882  pcadd  12884  pcmpt  12887  expnprm  12897  pockthg  12901  infpnlem2  12904  prmunb  12906  1arith  12911  4sqlem10  12931  4sqlem11  12945  4sqlem12  12946  4sqlem13m  12947  4sqlem17  12951  4sqlem18  12952  ennnfonelemex  13006  ennnfonelemhom  13007  ennnfonelemrnh  13008  ennnfonelemnn0  13014  ennnfonelemim  13016  exmidunben  13018  ctinfomlemom  13019  ctinfom  13020  ctinf  13022  omctfn  13035  nninfdclemp1  13042  setscomd  13094  imasaddfnlemg  13368  mhmf1o  13524  grpinveu  13592  grpasscan1  13617  dfgrp3mlem  13652  grp1inv  13661  issubg4m  13751  ghmf1o  13833  srgisid  13970  ringadd2  14011  ringinvnzdiv  14034  unitgrp  14101  ringelnzr  14172  lringuplu  14181  subrguss  14221  subrgintm  14228  aprcotr  14270  islmodd  14278  lssclg  14349  lss0cl  14354  lssvneln0  14358  lss1d  14368  lmodindp1  14413  rnglidlmmgm  14481  znidomb  14643  znunit  14644  znrrg  14645  mplsubgfilemcl  14684  mplsubgfileminv  14685  tgcl  14759  neii1  14842  neii2  14844  neiss  14845  tpnei  14855  tgrest  14864  ssrest  14877  icnpimaex  14906  lmcvg  14912  cnpnei  14914  cnptopco  14917  lmff  14944  txcnp  14966  txcn  14970  hmeontr  15008  blssec  15133  mopni3  15179  blsscls2  15188  comet  15194  bdxmet  15196  bdmopn  15199  xmettxlem  15204  xmettx  15205  addcncntoplem  15256  mpomulcn  15261  mulc1cncf  15284  cncfco  15286  cncfmptc  15291  mulcncflem  15302  mulcncf  15303  dedekindeulemlu  15316  dedekindeulemeu  15317  suplociccreex  15319  suplociccex  15320  dedekindicclemlu  15325  dedekindicclemeu  15326  ivthinclemlopn  15331  ivthinclemlr  15332  ivthinclemuopn  15333  ivthinclemur  15334  ivthinclemloc  15336  ivthinc  15338  ivthreinc  15340  ivthdichlem  15346  limcimolemlt  15359  limcresi  15361  cnplimcim  15362  cnplimclemle  15363  cnplimclemr  15364  limccnpcntop  15370  limccoap  15373  dvcoapbr  15402  dvcj  15404  plyf  15432  plyaddlem1  15442  plymullem1  15443  plyco  15454  plycj  15456  plycn  15457  plyrecj  15458  dvply2g  15461  efltlemlt  15469  sin0pilem2  15477  tangtx  15533  logdivlti  15576  rplogbval  15640  logbgcd1irraplemexp  15663  logbgcd1irraplemap  15664  logbgcd1irrap  15665  perfect1  15693  perfectlem1  15694  perfectlem2  15695  lgsval4a  15722  lgsdir2lem3  15730  lgsne0  15738  gausslemma2dlem3  15763  gausslemma2dlem4  15764  gausslemma2dlem6  15767  gausslemma2dlem7  15768  gausslemma2d  15769  lgseisenlem1  15770  lgsquadlem2  15778  lgsquadlem3  15779  lgsquad2lem2  15782  lgsquad3  15784  2lgsoddprmlem2  15806  2sqlem8a  15822  2sqlem8  15823  2sqlem9  15824  lpvtx  15900  upgrex  15924  edgupgren  15960  umgredg  15964  upgrpredgv  15965  upgredg2vtx  15967  upgredgpr  15968  uspgrf1oedg  15995  usgredg4  16034  uspgredgdomord  16048  usgr1vr  16067  wlkvtxiedg  16117  wlkvtxiedgg  16118  wlk1walkdom  16131  upgriswlkdc  16132  upgrwlkedg  16133  uspgr2wlkeq  16137  uspgr2wlkeqi  16139  umgrwlknloop  16140  bj-exlimmpi  16243  uzdcinzz  16271  bj-charfundcALT  16281  bj-2inf  16410  bj-peano4  16427  bj-nn0suc  16436  1dom1el  16463  pw1ndom3  16467  subctctexmid  16479  nninfalllem1  16488  nninfsellemqall  16495  nninfomnilem  16498  nninffeq  16500  nnnninfex  16502  exmidsbthrlem  16504  sbthomlem  16507  refeq  16510  isomninnlem  16512  apdifflemr  16529  redcwlpo  16537  reap0  16540  nconstwlpolem  16547