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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-2 7

This theorem is used 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  437  pm2.21dd  629  mt2d  634  mpnanrd  704  mpjaod  730  stdcndcOLD  858  impidc  870  jadc  875  pm2.54dc  903  oplem1  988  mp3and  1381  xor3dc  1436  exlimdd  1925  exlimddv  1954  eqrdav  2237  necon1aidc  2471  necon1bidc  2472  necon4aidc  2488  reximddv  2653  reximssdv  2654  rexlimddv  2673  vtoclgft  2873  rspcedvd  2935  sseldd  3249  ssneldd  3251  tpid3g  3828  preq12b  3895  axpweq  4310  exmid1dc  4339  exmid1stab  4347  opth  4379  issod  4466  frirrg  4497  frind  4499  ralxfr2d  4612  rexxfr2d  4613  eldifpw  4625  onun2  4639  onuni  4643  elirr  4690  en2lp  4703  wetriext  4726  peano2  4744  relop  4932  elres  5101  sotri2  5188  iota4an  5361  iota5  5362  funeu  5405  funopg  5414  imadiflem  5463  funimaexglem  5467  ssimaex  5767  ffvelcdm  5844  dff3im  5856  dffo4  5859  funopsn  5894  f1eqcocnv  6000  f1oiso2  6036  riota5f  6068  riotass2  6070  acexmidlemcase  6083  elovimad  6132  ovmpodf  6223  ovmpodv2  6225  ovi3  6229  ov6g  6230  caoftrn  6339  op1steq  6417  fvdifsuppst  6488  suppssdc  6504  suppofss1dcl  6508  suppofss2dcl  6509  tfr0dm  6598  tfrlemibxssdm  6603  tfrlemi14d  6609  tfr1onlembxssdm  6619  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllembxssdm  6632  tfrcllemaccex  6637  tfrcllemres  6638  rdgivallem  6657  nnsucelsuc  6769  nnsucsssuc  6770  dcdifsnid  6782  nnawordex  6807  ersym  6824  mapvalg  6937  pmvalg  6938  mapsnd  6976  mapsn  6978  fundmen  7100  1dom1el  7113  en2  7118  pw2f1odclem  7140  mapdom1g  7153  fidceq  7177  fin0or  7196  findcard2  7199  findcard2s  7200  fidcen  7209  prfidceq  7241  fiintim  7244  funisfsuppdc  7299  suplub2ti  7348  supsnti  7352  supisoex  7356  difinfsnlem  7446  difinfsn  7447  ctm  7456  ctssdclemn0  7457  ctssdccl  7458  ctssdc  7460  enumctlemm  7461  nninfninc  7470  nnnninfeq2  7476  enomnilem  7485  exmidomniim  7488  exmidomni  7489  fodjuomnilemdc  7491  fodjuomnilemres  7495  omnimkv  7503  mkvprop  7505  omniwomnimkv  7514  en2prde  7546  pr2cv1  7548  en2eleq  7554  acfun  7570  exmidontriimlem1  7584  exmidontriimlem4  7587  exmidontriim  7588  papsym  7619  papcotr  7620  ccfunen  7637  cc4f  7642  cc4n  7644  elni2  7688  mulclpi  7702  nlt1pig  7715  indpi  7716  recclnq  7766  ltexnqq  7782  halfnqq  7784  prarloclemarch  7792  prarloclemarch2  7793  prop  7849  prltlu  7861  prarloclem3step  7870  prarloclem5  7874  prarloclem  7875  prarloc  7877  prarloc2  7878  genpml  7891  genpmu  7892  genprndl  7895  genprndu  7896  genpdisj  7897  addnqprllem  7901  addnqprulem  7902  addlocprlemeq  7907  addlocprlemgt  7908  addlocprlem  7909  addlocpr  7910  nqprloc  7919  nqprl  7925  nqpru  7926  addnqprlemrl  7931  addnqprlemru  7932  appdivnq  7937  prmuloc  7940  prmuloc2  7941  mullocprlem  7944  mullocpr  7945  mulnqprlemrl  7947  mulnqprlemru  7948  ltprordil  7963  ltpopr  7969  ltsopr  7970  ltaddpr  7971  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemlol  7976  ltexprlemopu  7977  ltexprlemupu  7978  ltexprlemloc  7981  ltexprlemfl  7983  ltexprlemrl  7984  ltexprlemfu  7985  ltexprlemru  7986  ltaprg  7993  recexprlemm  7998  recexprlem1ssl  8007  recexprlem1ssu  8008  aptiprleml  8013  aptiprlemu  8014  archpr  8017  cauappcvgprlemm  8019  cauappcvgprlemopl  8020  cauappcvgprlemlol  8021  cauappcvgprlemopu  8022  cauappcvgprlemupu  8023  cauappcvgprlemdisj  8025  cauappcvgprlemloc  8026  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  cauappcvgprlemladdru  8030  cauappcvgprlem1  8033  archrecpr  8038  caucvgprlemnkj  8040  caucvgprlemnbj  8041  caucvgprlemm  8042  caucvgprlemopl  8043  caucvgprlemlol  8044  caucvgprlemopu  8045  caucvgprlemupu  8046  caucvgprlemdisj  8048  caucvgprlemloc  8049  caucvgprlemladdfu  8051  caucvgprlem1  8053  caucvgprlemlim  8055  caucvgprprlemnbj  8067  caucvgprprlemml  8068  caucvgprprlemopl  8071  caucvgprprlemlol  8072  caucvgprprlemopu  8073  caucvgprprlemupu  8074  caucvgprprlemdisj  8076  caucvgprprlemloc  8077  caucvgprprlemexbt  8080  caucvgprprlemaddq  8082  caucvgprprlemlim  8085  suplocexprlemss  8089  suplocexprlemrl  8091  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemdisj  8094  suplocexprlemloc  8095  suplocexprlemub  8097  suplocexprlemlub  8098  recexgt0sr  8147  mulgt0sr  8152  archsr  8156  caucvgsrlemoffcau  8172  suplocsrlemb  8180  suplocsrlempr  8181  suplocsrlem  8182  cnm  8206  axarch  8265  axcaucvglemcau  8272  axpre-suploclemres  8275  lelttr  8421  ltletr  8422  ltled  8453  cnegexlem1  8509  cnegexlem2  8510  renegcl  8595  negf1o  8717  gt0add  8910  apreap  8924  apirr  8942  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  mulap0r  8952  apti  8959  aprcl  8983  aptap  8987  recexap  8990  mulap0  8991  receuap  9008  mul0eqap  9009  lep1  9184  lem1  9186  letrp1  9187  recreclt  9239  lbinf  9287  suprubex  9290  nnrecgt0  9352  bndndx  9574  nn0ge2m1nn  9637  elnn0z  9667  peano2z  9690  zaddcl  9694  ztri3or0  9696  zltnle  9700  zdceq  9730  zdcle  9731  zdclt  9732  zdiv  9745  zeo  9762  fnn0ind  9773  btwnz  9776  uzm1  9969  uzp1  9972  indstr  10009  supinfneg  10011  infsupneg  10012  eluzdc  10026  nn01to3  10033  qapne  10055  xrltled  10218  xrlelttr  10225  xrltletr  10226  ge0nemnf  10243  fzdcel  10461  elfzouz2  10586  fzoss1  10597  fzospliti  10602  elincfzoext  10628  fzocatel  10634  fzostep1  10673  zsupcllemstep  10679  zsupcl  10681  infssuzledc  10684  qtri3or  10692  qltnle  10695  qdceq  10696  qdclt  10697  exbtwnzlemex  10701  rebtwn2zlemstep  10704  rebtwn2z  10706  qbtwnxr  10709  ioom  10712  ico0  10713  ioc0  10714  flqeqceilz  10776  modqadd1  10819  modqmul1  10835  frec2uzuzd  10860  frec2uzlt2d  10862  frec2uzf1od  10864  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgdomlem  10875  uzsinds  10902  seqvalcd  10919  seqovcd  10925  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  monoord  10943  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  iseqf1olemab  10960  iseqf1olemnanb  10961  iseqf1olemqk  10965  seqf1oglem1  10977  seqf1og  10979  seq3id3  10982  seq3id2  10984  seq3homo  10985  seqhomog  10988  expgt1  11035  m1expeven  11044  expnbnd  11122  expnlbnd2  11124  nn0ltexp2  11169  apexp1  11178  hashennn  11241  hashfibclem  11304  hashf1lem2  11308  zfz1isolem1  11314  seq3coll  11316  pfxwrdsymbg  11484  wrdind  11516  wrd2ind  11517  cjap  11694  caucvgre  11769  cvg1nlemres  11773  resqrexlemgt0  11808  resqrexlemglsq  11810  resqrexlemga  11811  resqrtcl  11817  abslt  11877  abssubap0  11879  abssubne0  11880  caubnd2  11906  qdenre  11991  maxabslemlub  11996  maxabs  11998  maxleast  12002  fimaxre2  12016  xrmaxiflemlub  12039  xrmaxif  12042  xrmaxltsup  12049  xrmaxadd  12052  xrmineqinf  12060  climuni  12084  2clim  12092  climcn1  12099  climcn2  12100  subcn2  12102  mulcn2  12103  climsqz  12126  climsqz2  12127  climcau  12138  climcvg1nlem  12140  climcaucn  12142  serf0  12143  sumrbdclem  12169  summodclem2  12174  zsumdc  12176  divcnv  12289  absltap  12301  absgtap  12302  mertenslem2  12328  ntrivcvgap  12340  prodrbdclem  12363  prodmodclem2  12369  zproddc  12371  prodssdc  12381  fprodsplitdc  12388  fprodcl2lem  12397  efcllemp  12450  tanvalap  12500  sin01bnd  12549  cos01bnd  12550  sin01gt0  12554  absef  12562  eirrap  12570  dvds0  12598  dvdsmul1  12605  dvdsmultr1d  12624  dvdslelemd  12635  divconjdvds  12641  alzdvds  12646  3dvds  12656  sqoddm1div8z  12678  nno  12698  divalglemex  12714  bits0o  12742  dvdsbnd  12758  dvdslegcd  12766  zeqzmulgcd  12772  gcd0id  12781  gcdaddm  12786  gcd1  12789  gcdabs  12790  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemex  12803  bezoutlemzz  12804  bezoutlemaz  12805  bezoutlembz  12806  bezoutlembi  12807  bezoutlemle  12810  bezoutlemsup  12811  mulgcd  12818  gcdzeq  12824  dvdsmulgcd  12827  sqgcd  12831  bezoutr1  12835  nninfctlemfo  12842  algcvga  12854  algfx  12855  eucalglt  12860  eucalg  12862  lcmneg  12877  lcmabs  12879  lcmgcdlem  12880  ncoprmgcdne1b  12892  mulgcddvds  12897  qredeq  12899  divgcdcoprm0  12904  cncongr1  12906  isprm2lem  12919  nprm  12926  dvdsnprmd  12928  prmdvdsfz  12943  isprm5lem  12945  coprm  12948  isprm6  12951  sqrt2irr  12966  pwbdvdslemn  12969  pwbdvdseulemle  12971  nnmaxpwlemdvds  12974  nnmaxpwlemndvds  12975  sqrt2irrap  12985  qnumdencl  12992  nn0sqdcq  13013  sqrtrirr  13014  prmdiv  13042  modprmn0modprm0  13064  prm23lt5  13071  pythagtriplem4  13076  pythagtriplem19  13090  pythagtrip  13091  pclemub  13095  pcpre1  13100  pcpremul  13101  pceulem  13102  pcqcl  13114  pcidlem  13131  pcgcd1  13136  pc2dvds  13138  dvdsprmpweqle  13145  difsqpwdvds  13146  pcadd  13148  pcmpt  13151  expnprm  13161  pockthg  13165  infpnlem2  13168  prmunb  13170  1arith  13175  4sqlem10  13195  4sqlem11  13209  4sqlem12  13210  4sqlem13m  13211  4sqlem17  13215  4sqlem18  13216  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfrceq  13330  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemrnh  13365  ennnfonelemnn0  13371  ennnfonelemim  13373  exmidunben  13375  ctinfomlemom  13376  ctinfom  13377  ctinf  13379  omctfn  13392  nninfdclemp1  13399  setscomd  13451  imasaddfnlemg  13694  mhmf1o  13836  grpinveu  13902  grpasscan1  13927  dfgrp3mlem  13962  grp1inv  13971  issubg4m  14055  ghmf1o  14137  gsum2d2fi  14274  srgisid  14397  ringadd2  14439  ringinvnzdiv  14462  unitgrp  14532  ringelnzr  14603  lringuplu  14612  subrguss  14653  subrgintm  14660  aprcotr  14706  islmodd  14738  lssclg  14810  lss0cl  14815  lssvneln0  14819  lss1d  14829  lmodindp1  14874  rnglidlmmgm  14942  znidomb  15102  znunit  15103  znrrg  15104  rnasclassa  15147  psrbagfsuppd  15193  mvrf1fi  15231  mplsubgfileminv  15247  tgcl  15323  neii1  15406  neii2  15408  neiss  15409  tpnei  15419  tgrest  15428  ssrest  15441  icnpimaex  15470  lmcvg  15476  cnpnei  15478  cnptopco  15481  lmff  15508  txcnp  15530  txcn  15534  hmeontr  15572  blssec  15697  mopni3  15743  blsscls2  15752  comet  15758  bdxmet  15760  bdmopn  15763  xmettxlem  15768  xmettx  15769  addcncntoplem  15820  mpomulcn  15825  mulc1cncf  15848  cncfco  15850  cncfmptc  15855  mulcncflem  15866  mulcncf  15867  dedekindeulemlu  15880  dedekindeulemeu  15881  suplociccreex  15883  suplociccex  15884  dedekindicclemlu  15889  dedekindicclemeu  15890  ivthinclemlopn  15895  ivthinclemlr  15896  ivthinclemuopn  15897  ivthinclemur  15898  ivthinclemloc  15900  ivthinc  15902  ivthreinc  15904  ivthdichlem  15910  limcimolemlt  15923  limcresi  15925  cnplimcim  15926  cnplimclemle  15927  cnplimclemr  15928  limccnpcntop  15934  limccoap  15937  dvcoapbr  15966  dvcj  15968  plyf  15996  plyaddlem1  16006  plymullem1  16007  plyco  16018  plycj  16020  plycn  16021  plyrecj  16022  dvply2g  16025  efltlemlt  16033  sin0pilem2  16042  tangtx  16098  logdivlti  16144  logdivlt  16157  rplogbval  16214  logbgcd1irraplemexp  16237  logbgcd1irraplemap  16238  logbgcd1irrap  16239  zprmlogbaplem2  16249  zprmlogbap  16251  birthdaylem1g  16258  ppiublem2  16325  chtublem  16328  chtqub  16329  perfect1  16331  perfectlem1  16332  perfectlem2  16333  bposlem6  16349  bposlem9  16352  bpos  16353  lgsval4a  16379  lgsdir2lem3  16387  lgsne0  16395  gausslemma2dlem3  16420  gausslemma2dlem4  16421  gausslemma2dlem6  16424  gausslemma2dlem7  16425  gausslemma2d  16426  lgseisenlem1  16427  lgsquadlem2  16435  lgsquadlem3  16436  lgsquad2lem2  16439  lgsquad3  16441  2lgsoddprmlem2  16463  2sqlem8a  16479  2sqlem8  16480  2sqlem9  16481  lpvtx  16558  upgrex  16582  upgr1een  16603  edgupgren  16620  umgredg  16624  upgrpredgv  16625  upgredg2vtx  16627  upgredgpr  16628  uspgrf1oedg  16655  usgredg4  16694  uspgredgdomord  16708  usgr1vr  16727  wlkvtxiedg  16824  wlkvtxiedgg  16825  wlk1walkdom  16838  upgriswlkdc  16839  upgrwlkedg  16840  uspgr2wlkeq  16844  uspgr2wlkeqi  16846  umgrwlknloop  16847  eupth2lem2dc  16938  trlsegvdeglem1  16939  eupth2lem3lem4fi  16952  bj-exlimmpi  17036  uzdcinzz  17064  bj-charfundcALT  17073  bj-2inf  17202  bj-peano4  17219  bj-nn0suc  17228  pw1ndom3  17258  subctctexmid  17268  exmidcon  17275  nninfalllem1  17290  nninfsellemqall  17297  nninfomnilem  17300  nninffeq  17302  nnnninfex  17304  exmidsbthrlem  17306  sbthomlem  17309  refeq  17312  isomninnlem  17318  apdifflemr  17336  redcwlpo  17345  reap0  17348  nconstwlpolem  17355