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

Syntax hints:   → wi 4

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

This theorem is referenced by:  syl  14  mpi  15  id  19  mpcom  36  mpdd  41  mp2d  47  pm2.43i  49  syl3c  63  mpbid  146  mpbird  166  jcai  307  mp2and  427  pm2.21dd  590  mt2d  595  mpjaod  679  impidc  799  jadc  804  pm2.54dc  834  stabtestimpdc  868  pm4.55dc  890  oplem1  927  mp3and  1286  xor3dc  1333  exlimdd  1811  exlimddv  1837  eqrdav  2099  necon1aidc  2318  necon1bidc  2319  necon4aidc  2335  reximddv  2494  reximssdv  2495  rexlimddv  2513  vtoclgft  2691  rspcedvd  2750  sseldd  3048  ssneldd  3050  tpid3g  3585  preq12b  3644  axpweq  4035  opth  4097  issod  4179  frirrg  4210  frind  4212  ralxfr2d  4323  rexxfr2d  4324  eldifpw  4336  onun2  4344  onuni  4348  elirr  4394  en2lp  4407  wetriext  4429  peano2  4447  relop  4627  elres  4791  sotri2  4872  iota4an  5043  iota5  5044  funeu  5084  funopg  5093  imadiflem  5138  funimaexglem  5142  ssimaex  5414  ffvelrn  5485  dff3im  5497  dffo4  5500  f1eqcocnv  5624  f1oiso2  5660  riota5f  5686  riotass2  5688  acexmidlemcase  5701  ovmpodf  5834  ovmpodv2  5836  ovi3  5839  ov6g  5840  caoftrn  5938  op1steq  6007  tfr0dm  6149  tfrlemibxssdm  6154  tfrlemi14d  6160  tfr1onlembxssdm  6170  tfr1onlemaccex  6175  tfr1onlemres  6176  tfrcllembxssdm  6183  tfrcllemaccex  6188  tfrcllemres  6189  rdgivallem  6208  nnsucelsuc  6317  nnsucsssuc  6318  dcdifsnid  6330  nnawordex  6354  ersym  6371  mapvalg  6482  pmvalg  6483  mapsn  6514  fundmen  6630  mapdom1g  6670  fidceq  6692  fin0or  6709  findcard2  6712  findcard2s  6713  fiintim  6746  suplub2ti  6803  supsnti  6807  supisoex  6811  difinfsnlem  6899  difinfsn  6900  ctm  6909  ctssdclemn0  6910  ctssdclemr  6911  ctssdc  6912  enumctlemm  6913  enomnilem  6922  exmidomniim  6925  exmidomni  6926  fodjuomnilemdc  6928  fodjuomnilemres  6932  omnimkv  6941  mkvprop  6943  en2eleq  6960  elni2  7023  mulclpi  7037  nlt1pig  7050  indpi  7051  recclnq  7101  ltexnqq  7117  halfnqq  7119  prarloclemarch  7127  prarloclemarch2  7128  prop  7184  prltlu  7196  prarloclem3step  7205  prarloclem5  7209  prarloclem  7210  prarloc  7212  prarloc2  7213  genpml  7226  genpmu  7227  genprndl  7230  genprndu  7231  genpdisj  7232  addnqprllem  7236  addnqprulem  7237  addlocprlemeq  7242  addlocprlemgt  7243  addlocprlem  7244  addlocpr  7245  nqprloc  7254  nqprl  7260  nqpru  7261  addnqprlemrl  7266  addnqprlemru  7267  appdivnq  7272  prmuloc  7275  prmuloc2  7276  mullocprlem  7279  mullocpr  7280  mulnqprlemrl  7282  mulnqprlemru  7283  ltprordil  7298  ltpopr  7304  ltsopr  7305  ltaddpr  7306  ltexprlemm  7309  ltexprlemopl  7310  ltexprlemlol  7311  ltexprlemopu  7312  ltexprlemupu  7313  ltexprlemloc  7316  ltexprlemfl  7318  ltexprlemrl  7319  ltexprlemfu  7320  ltexprlemru  7321  ltaprg  7328  recexprlemm  7333  recexprlem1ssl  7342  recexprlem1ssu  7343  aptiprleml  7348  aptiprlemu  7349  archpr  7352  cauappcvgprlemm  7354  cauappcvgprlemopl  7355  cauappcvgprlemlol  7356  cauappcvgprlemopu  7357  cauappcvgprlemupu  7358  cauappcvgprlemdisj  7360  cauappcvgprlemloc  7361  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  cauappcvgprlemladdru  7365  cauappcvgprlem1  7368  archrecpr  7373  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemm  7377  caucvgprlemopl  7378  caucvgprlemlol  7379  caucvgprlemopu  7380  caucvgprlemupu  7381  caucvgprlemdisj  7383  caucvgprlemloc  7384  caucvgprlemladdfu  7386  caucvgprlem1  7388  caucvgprlemlim  7390  caucvgprprlemnbj  7402  caucvgprprlemml  7403  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemopu  7408  caucvgprprlemupu  7409  caucvgprprlemdisj  7411  caucvgprprlemloc  7412  caucvgprprlemexbt  7415  caucvgprprlemaddq  7417  caucvgprprlemlim  7420  recexgt0sr  7469  mulgt0sr  7473  archsr  7477  caucvgsrlemoffcau  7493  axarch  7576  axcaucvglemcau  7583  lelttr  7723  ltletr  7724  ltled  7752  cnegexlem1  7808  cnegexlem2  7809  renegcl  7894  negf1o  8011  gt0add  8201  apreap  8215  apirr  8233  apsym  8234  apcotr  8235  apadd1  8236  apneg  8239  mulext1  8240  mulap0r  8243  apti  8250  recexap  8275  mulap0  8276  receuap  8291  mul0eqap  8292  lep1  8461  lem1  8463  letrp1  8464  recreclt  8516  lbinf  8564  suprubex  8567  nnrecgt0  8616  bndndx  8828  nn0ge2m1nn  8889  elnn0z  8919  peano2z  8942  zaddcl  8946  ztri3or0  8948  zltnle  8952  zdceq  8978  zdcle  8979  zdclt  8980  zdiv  8991  zeo  9008  fnn0ind  9019  btwnz  9022  uzm1  9206  uzp1  9209  indstr  9238  supinfneg  9240  infsupneg  9241  eluzdc  9254  nn01to3  9259  qapne  9281  xrltled  9426  xrlelttr  9430  xrltletr  9431  ge0nemnf  9448  fzdcel  9661  elfzouz2  9779  fzoss1  9789  fzospliti  9794  fzocatel  9817  fzostep1  9855  qtri3or  9861  qltnle  9864  qdceq  9865  exbtwnzlemex  9868  rebtwn2zlemstep  9871  rebtwn2z  9873  qbtwnxr  9876  ioom  9879  ico0  9880  ioc0  9881  flqeqceilz  9932  modqadd1  9975  modqmul1  9991  frec2uzuzd  10016  frec2uzlt2d  10018  frec2uzf1od  10020  frecuzrdgrrn  10022  frec2uzrdg  10023  frecuzrdgrcl  10024  frecuzrdgsuc  10028  frecuzrdgrclt  10029  frecuzrdgdomlem  10031  uzsinds  10056  seqvalcd  10073  seqovcd  10077  seq3fveq2  10083  seq3shft2  10087  monoord  10090  seq3split  10093  seq3caopr3  10095  iseqf1olemab  10103  iseqf1olemnanb  10104  iseqf1olemqk  10108  seq3id3  10121  seq3id2  10123  seq3homo  10124  expgt1  10172  m1expeven  10181  expnbnd  10256  expnlbnd2  10258  hashennn  10367  zfz1isolem1  10424  seq3coll  10426  cjap  10519  caucvgre  10593  cvg1nlemres  10597  resqrexlemgt0  10632  resqrexlemglsq  10634  resqrexlemga  10635  resqrtcl  10641  abslt  10700  abssubap0  10702  abssubne0  10703  caubnd2  10729  qdenre  10814  maxabslemlub  10819  maxabs  10821  maxleast  10825  fimaxre2  10837  xrmaxiflemlub  10856  xrmaxif  10859  xrmaxltsup  10866  xrmaxadd  10869  xrmineqinf  10877  climuni  10901  2clim  10909  climcn1  10916  climcn2  10917  subcn2  10919  mulcn2  10920  climsqz  10943  climsqz2  10944  climcau  10955  climcvg1nlem  10957  climcaucn  10959  serf0  10960  sumrbdclem  10984  summodclem2  10990  zsumdc  10992  divcnv  11105  absltap  11117  absgtap  11118  mertenslem2  11144  efcllemp  11162  tanvalap  11213  sin01bnd  11262  cos01bnd  11263  sin01gt0  11266  absef  11273  eirrap  11279  dvds0  11303  dvdsmul1  11310  dvdsmultr1d  11327  dvdslelemd  11336  divconjdvds  11342  alzdvds  11347  sqoddm1div8z  11378  nno  11398  divalglemex  11414  zsupcllemstep  11433  zsupcl  11435  infssuzledc  11438  dvdsbnd  11440  dvdslegcd  11448  zeqzmulgcd  11454  gcd0id  11462  gcdaddm  11467  gcd1  11470  gcdabs  11471  bezoutlemnewy  11477  bezoutlemstep  11478  bezoutlemmain  11479  bezoutlemex  11482  bezoutlemzz  11483  bezoutlemaz  11484  bezoutlembz  11485  bezoutlembi  11486  bezoutlemle  11489  bezoutlemsup  11490  mulgcd  11497  gcdzeq  11503  dvdsmulgcd  11506  sqgcd  11510  bezoutr1  11514  algcvga  11525  algfx  11526  eucalglt  11531  eucalg  11533  lcmneg  11548  lcmabs  11550  lcmgcdlem  11551  ncoprmgcdne1b  11563  mulgcddvds  11568  qredeq  11570  divgcdcoprm0  11575  cncongr1  11577  isprm2lem  11590  nprm  11597  dvdsnprmd  11599  prmdvdsfz  11612  coprm  11615  isprm6  11618  sqrt2irr  11633  pw2dvdslemn  11635  pw2dvdseulemle  11637  oddpwdclemdvds  11640  oddpwdclemndvds  11641  sqrt2irrap  11650  qnumdencl  11657  ennnfonelemex  11719  ennnfonelemhom  11720  ennnfonelemrnh  11721  ennnfonelemnn0  11727  ennnfonelemim  11729  exmidunben  11731  ctinfomlemom  11732  ctinfom  11733  ctinf  11735  tgcl  12015  neii1  12098  neii2  12100  neiss  12101  tpnei  12111  tgrest  12120  ssrest  12133  icnpimaex  12161  lmcvg  12167  cnpnei  12169  cnptopco  12172  lmff  12199  txcnp  12221  txcn  12225  blssec  12366  mopni3  12412  blsscls2  12421  comet  12427  bdxmet  12429  bdmopn  12432  mulc1cncf  12489  cncfco  12491  cncfmptc  12495  mulcncflem  12502  mulcncf  12503  limcimolemlt  12513  limcresi  12515  cnplimcim  12516  limccnpcntop  12520  bj-exlimmpi  12559  uzdcinzz  12586  bj-2inf  12721  bj-peano4  12738  bj-nn0suc  12747  nninfalllem1  12787  nninfsellemqall  12795  nninfomnilem  12798  nninffeq  12800  exmidsbthrlem  12801  sbthomlem  12804  refeq  12807  isomninnlem  12809