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  621  mt2d  626  mpjaod  720  stdcndcOLD  848  impidc  860  jadc  865  pm2.54dc  893  oplem1  978  mp3and  1353  xor3dc  1407  exlimdd  1896  exlimddv  1923  eqrdav  2205  necon1aidc  2428  necon1bidc  2429  necon4aidc  2445  reximddv  2610  reximssdv  2611  rexlimddv  2629  vtoclgft  2824  rspcedvd  2884  sseldd  3195  ssneldd  3197  tpid3g  3749  preq12b  3813  axpweq  4219  exmid1dc  4248  exmid1stab  4256  opth  4285  issod  4370  frirrg  4401  frind  4403  ralxfr2d  4515  rexxfr2d  4516  eldifpw  4528  onun2  4542  onuni  4546  elirr  4593  en2lp  4606  wetriext  4629  peano2  4647  relop  4832  elres  5000  sotri2  5085  iota4an  5257  iota5  5258  funeu  5301  funopg  5310  imadiflem  5358  funimaexglem  5362  ssimaex  5647  ffvelcdm  5720  dff3im  5732  dffo4  5735  funopsn  5769  f1eqcocnv  5867  f1oiso2  5903  riota5f  5931  riotass2  5933  acexmidlemcase  5946  ovmpodf  6084  ovmpodv2  6086  ovi3  6090  ov6g  6091  caoftrn  6198  op1steq  6272  tfr0dm  6415  tfrlemibxssdm  6420  tfrlemi14d  6426  tfr1onlembxssdm  6436  tfr1onlemaccex  6441  tfr1onlemres  6442  tfrcllembxssdm  6449  tfrcllemaccex  6454  tfrcllemres  6455  rdgivallem  6474  nnsucelsuc  6584  nnsucsssuc  6585  dcdifsnid  6597  nnawordex  6622  ersym  6639  mapvalg  6752  pmvalg  6753  mapsn  6784  fundmen  6905  en2  6919  pw2f1odclem  6938  mapdom1g  6951  fidceq  6973  fin0or  6990  findcard2  6993  findcard2s  6994  prfidceq  7032  fiintim  7035  suplub2ti  7110  supsnti  7114  supisoex  7118  difinfsnlem  7208  difinfsn  7209  ctm  7218  ctssdclemn0  7219  ctssdccl  7220  ctssdc  7222  enumctlemm  7223  nninfninc  7232  nnnninfeq2  7238  enomnilem  7247  exmidomniim  7250  exmidomni  7251  fodjuomnilemdc  7253  fodjuomnilemres  7257  omnimkv  7265  mkvprop  7267  omniwomnimkv  7276  en2eleq  7310  acfun  7326  exmidontriimlem1  7340  exmidontriimlem4  7343  exmidontriim  7344  ccfunen  7383  cc4f  7388  cc4n  7390  elni2  7434  mulclpi  7448  nlt1pig  7461  indpi  7462  recclnq  7512  ltexnqq  7528  halfnqq  7530  prarloclemarch  7538  prarloclemarch2  7539  prop  7595  prltlu  7607  prarloclem3step  7616  prarloclem5  7620  prarloclem  7621  prarloc  7623  prarloc2  7624  genpml  7637  genpmu  7638  genprndl  7641  genprndu  7642  genpdisj  7643  addnqprllem  7647  addnqprulem  7648  addlocprlemeq  7653  addlocprlemgt  7654  addlocprlem  7655  addlocpr  7656  nqprloc  7665  nqprl  7671  nqpru  7672  addnqprlemrl  7677  addnqprlemru  7678  appdivnq  7683  prmuloc  7686  prmuloc2  7687  mullocprlem  7690  mullocpr  7691  mulnqprlemrl  7693  mulnqprlemru  7694  ltprordil  7709  ltpopr  7715  ltsopr  7716  ltaddpr  7717  ltexprlemm  7720  ltexprlemopl  7721  ltexprlemlol  7722  ltexprlemopu  7723  ltexprlemupu  7724  ltexprlemloc  7727  ltexprlemfl  7729  ltexprlemrl  7730  ltexprlemfu  7731  ltexprlemru  7732  ltaprg  7739  recexprlemm  7744  recexprlem1ssl  7753  recexprlem1ssu  7754  aptiprleml  7759  aptiprlemu  7760  archpr  7763  cauappcvgprlemm  7765  cauappcvgprlemopl  7766  cauappcvgprlemlol  7767  cauappcvgprlemopu  7768  cauappcvgprlemupu  7769  cauappcvgprlemdisj  7771  cauappcvgprlemloc  7772  cauappcvgprlemladdfu  7774  cauappcvgprlemladdfl  7775  cauappcvgprlemladdru  7776  cauappcvgprlem1  7779  archrecpr  7784  caucvgprlemnkj  7786  caucvgprlemnbj  7787  caucvgprlemm  7788  caucvgprlemopl  7789  caucvgprlemlol  7790  caucvgprlemopu  7791  caucvgprlemupu  7792  caucvgprlemdisj  7794  caucvgprlemloc  7795  caucvgprlemladdfu  7797  caucvgprlem1  7799  caucvgprlemlim  7801  caucvgprprlemnbj  7813  caucvgprprlemml  7814  caucvgprprlemopl  7817  caucvgprprlemlol  7818  caucvgprprlemopu  7819  caucvgprprlemupu  7820  caucvgprprlemdisj  7822  caucvgprprlemloc  7823  caucvgprprlemexbt  7826  caucvgprprlemaddq  7828  caucvgprprlemlim  7831  suplocexprlemss  7835  suplocexprlemrl  7837  suplocexprlemmu  7838  suplocexprlemru  7839  suplocexprlemdisj  7840  suplocexprlemloc  7841  suplocexprlemub  7843  suplocexprlemlub  7844  recexgt0sr  7893  mulgt0sr  7898  archsr  7902  caucvgsrlemoffcau  7918  suplocsrlemb  7926  suplocsrlempr  7927  suplocsrlem  7928  cnm  7952  axarch  8011  axcaucvglemcau  8018  axpre-suploclemres  8021  lelttr  8168  ltletr  8169  ltled  8198  cnegexlem1  8254  cnegexlem2  8255  renegcl  8340  negf1o  8461  gt0add  8653  apreap  8667  apirr  8685  apsym  8686  apcotr  8687  apadd1  8688  apneg  8691  mulext1  8692  mulap0r  8695  apti  8702  aprcl  8726  aptap  8730  recexap  8733  mulap0  8734  receuap  8749  mul0eqap  8750  lep1  8925  lem1  8927  letrp1  8928  recreclt  8980  lbinf  9028  suprubex  9031  nnrecgt0  9081  bndndx  9301  nn0ge2m1nn  9362  elnn0z  9392  peano2z  9415  zaddcl  9419  ztri3or0  9421  zltnle  9425  zdceq  9455  zdcle  9456  zdclt  9457  zdiv  9468  zeo  9485  fnn0ind  9496  btwnz  9499  uzm1  9686  uzp1  9689  indstr  9721  supinfneg  9723  infsupneg  9724  eluzdc  9738  nn01to3  9745  qapne  9767  xrltled  9928  xrlelttr  9935  xrltletr  9936  ge0nemnf  9953  fzdcel  10169  elfzouz2  10291  fzoss1  10302  fzospliti  10307  elincfzoext  10329  fzocatel  10335  fzostep1  10373  zsupcllemstep  10379  zsupcl  10381  infssuzledc  10384  qtri3or  10390  qltnle  10393  qdceq  10394  qdclt  10395  exbtwnzlemex  10399  rebtwn2zlemstep  10402  rebtwn2z  10404  qbtwnxr  10407  ioom  10410  ico0  10411  ioc0  10412  flqeqceilz  10470  modqadd1  10513  modqmul1  10529  frec2uzuzd  10554  frec2uzlt2d  10556  frec2uzf1od  10558  frecuzrdgrrn  10560  frec2uzrdg  10561  frecuzrdgrcl  10562  frecuzrdgsuc  10566  frecuzrdgrclt  10567  frecuzrdgdomlem  10569  uzsinds  10596  seqvalcd  10613  seqovcd  10619  seq3fveq2  10627  seqfveq2g  10629  seq3shft2  10633  seqshft2g  10634  monoord  10637  seq3split  10640  seqsplitg  10641  seq3caopr3  10643  iseqf1olemab  10654  iseqf1olemnanb  10655  iseqf1olemqk  10659  seqf1oglem1  10671  seqf1og  10673  seq3id3  10676  seq3id2  10678  seq3homo  10679  seqhomog  10682  expgt1  10729  m1expeven  10738  expnbnd  10815  expnlbnd2  10817  nn0ltexp2  10861  apexp1  10870  hashennn  10932  zfz1isolem1  10992  seq3coll  10994  pfxwrdsymbg  11149  cjap  11261  caucvgre  11336  cvg1nlemres  11340  resqrexlemgt0  11375  resqrexlemglsq  11377  resqrexlemga  11378  resqrtcl  11384  abslt  11443  abssubap0  11445  abssubne0  11446  caubnd2  11472  qdenre  11557  maxabslemlub  11562  maxabs  11564  maxleast  11568  fimaxre2  11582  xrmaxiflemlub  11603  xrmaxif  11606  xrmaxltsup  11613  xrmaxadd  11616  xrmineqinf  11624  climuni  11648  2clim  11656  climcn1  11663  climcn2  11664  subcn2  11666  mulcn2  11667  climsqz  11690  climsqz2  11691  climcau  11702  climcvg1nlem  11704  climcaucn  11706  serf0  11707  sumrbdclem  11732  summodclem2  11737  zsumdc  11739  divcnv  11852  absltap  11864  absgtap  11865  mertenslem2  11891  ntrivcvgap  11903  prodrbdclem  11926  prodmodclem2  11932  zproddc  11934  prodssdc  11944  fprodsplitdc  11951  fprodcl2lem  11960  efcllemp  12013  tanvalap  12063  sin01bnd  12112  cos01bnd  12113  sin01gt0  12117  absef  12125  eirrap  12133  dvds0  12161  dvdsmul1  12168  dvdsmultr1d  12187  dvdslelemd  12198  divconjdvds  12204  alzdvds  12209  3dvds  12219  sqoddm1div8z  12241  nno  12261  divalglemex  12277  bits0o  12305  dvdsbnd  12321  dvdslegcd  12329  zeqzmulgcd  12335  gcd0id  12344  gcdaddm  12349  gcd1  12352  gcdabs  12353  bezoutlemnewy  12361  bezoutlemstep  12362  bezoutlemmain  12363  bezoutlemex  12366  bezoutlemzz  12367  bezoutlemaz  12368  bezoutlembz  12369  bezoutlembi  12370  bezoutlemle  12373  bezoutlemsup  12374  mulgcd  12381  gcdzeq  12387  dvdsmulgcd  12390  sqgcd  12394  bezoutr1  12398  nninfctlemfo  12405  algcvga  12417  algfx  12418  eucalglt  12423  eucalg  12425  lcmneg  12440  lcmabs  12442  lcmgcdlem  12443  ncoprmgcdne1b  12455  mulgcddvds  12460  qredeq  12462  divgcdcoprm0  12467  cncongr1  12469  isprm2lem  12482  nprm  12489  dvdsnprmd  12491  prmdvdsfz  12505  isprm5lem  12507  coprm  12510  isprm6  12513  sqrt2irr  12528  pw2dvdslemn  12531  pw2dvdseulemle  12533  oddpwdclemdvds  12536  oddpwdclemndvds  12537  sqrt2irrap  12546  qnumdencl  12553  prmdiv  12601  modprmn0modprm0  12623  prm23lt5  12630  pythagtriplem4  12635  pythagtriplem19  12649  pythagtrip  12650  pclemub  12654  pcpre1  12659  pcpremul  12660  pceulem  12661  pcqcl  12673  pcidlem  12690  pcgcd1  12695  pc2dvds  12697  dvdsprmpweqle  12704  difsqpwdvds  12705  pcadd  12707  pcmpt  12710  expnprm  12720  pockthg  12724  infpnlem2  12727  prmunb  12729  1arith  12734  4sqlem10  12754  4sqlem11  12768  4sqlem12  12769  4sqlem13m  12770  4sqlem17  12774  4sqlem18  12775  ennnfonelemex  12829  ennnfonelemhom  12830  ennnfonelemrnh  12831  ennnfonelemnn0  12837  ennnfonelemim  12839  exmidunben  12841  ctinfomlemom  12842  ctinfom  12843  ctinf  12845  omctfn  12858  nninfdclemp1  12865  setscomd  12917  imasaddfnlemg  13190  mhmf1o  13346  grpinveu  13414  grpasscan1  13439  dfgrp3mlem  13474  grp1inv  13483  issubg4m  13573  ghmf1o  13655  srgisid  13792  ringadd2  13833  ringinvnzdiv  13856  unitgrp  13922  ringelnzr  13993  lringuplu  14002  subrguss  14042  subrgintm  14049  aprcotr  14091  islmodd  14099  lssclg  14170  lss0cl  14175  lssvneln0  14179  lss1d  14189  lmodindp1  14234  rnglidlmmgm  14302  znidomb  14464  znunit  14465  znrrg  14466  mplsubgfilemcl  14505  mplsubgfileminv  14506  tgcl  14580  neii1  14663  neii2  14665  neiss  14666  tpnei  14676  tgrest  14685  ssrest  14698  icnpimaex  14727  lmcvg  14733  cnpnei  14735  cnptopco  14738  lmff  14765  txcnp  14787  txcn  14791  hmeontr  14829  blssec  14954  mopni3  15000  blsscls2  15009  comet  15015  bdxmet  15017  bdmopn  15020  xmettxlem  15025  xmettx  15026  addcncntoplem  15077  mpomulcn  15082  mulc1cncf  15105  cncfco  15107  cncfmptc  15112  mulcncflem  15123  mulcncf  15124  dedekindeulemlu  15137  dedekindeulemeu  15138  suplociccreex  15140  suplociccex  15141  dedekindicclemlu  15146  dedekindicclemeu  15147  ivthinclemlopn  15152  ivthinclemlr  15153  ivthinclemuopn  15154  ivthinclemur  15155  ivthinclemloc  15157  ivthinc  15159  ivthreinc  15161  ivthdichlem  15167  limcimolemlt  15180  limcresi  15182  cnplimcim  15183  cnplimclemle  15184  cnplimclemr  15185  limccnpcntop  15191  limccoap  15194  dvcoapbr  15223  dvcj  15225  plyf  15253  plyaddlem1  15263  plymullem1  15264  plyco  15275  plycj  15277  plycn  15278  plyrecj  15279  dvply2g  15282  efltlemlt  15290  sin0pilem2  15298  tangtx  15354  logdivlti  15397  rplogbval  15461  logbgcd1irraplemexp  15484  logbgcd1irraplemap  15485  logbgcd1irrap  15486  perfect1  15514  perfectlem1  15515  perfectlem2  15516  lgsval4a  15543  lgsdir2lem3  15551  lgsne0  15559  gausslemma2dlem3  15584  gausslemma2dlem4  15585  gausslemma2dlem6  15588  gausslemma2dlem7  15589  gausslemma2d  15590  lgseisenlem1  15591  lgsquadlem2  15599  lgsquadlem3  15600  lgsquad2lem2  15603  lgsquad3  15605  2lgsoddprmlem2  15627  2sqlem8a  15643  2sqlem8  15644  2sqlem9  15645  lpvtx  15719  bj-exlimmpi  15780  uzdcinzz  15808  bj-charfundcALT  15819  bj-2inf  15948  bj-peano4  15965  bj-nn0suc  15974  1dom1el  16001  subctctexmid  16011  nninfalllem1  16019  nninfsellemqall  16026  nninfomnilem  16029  nninffeq  16031  nnnninfex  16033  exmidsbthrlem  16035  sbthomlem  16038  refeq  16041  isomninnlem  16043  apdifflemr  16060  redcwlpo  16068  reap0  16071  nconstwlpolem  16078