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  719  stdcndcOLD  847  impidc  859  jadc  864  pm2.54dc  892  oplem1  977  mp3and  1351  xor3dc  1398  exlimdd  1883  exlimddv  1910  eqrdav  2192  necon1aidc  2415  necon1bidc  2416  necon4aidc  2432  reximddv  2597  reximssdv  2598  rexlimddv  2616  vtoclgft  2810  rspcedvd  2870  sseldd  3180  ssneldd  3182  tpid3g  3733  preq12b  3796  axpweq  4200  exmid1dc  4229  exmid1stab  4237  opth  4266  issod  4350  frirrg  4381  frind  4383  ralxfr2d  4495  rexxfr2d  4496  eldifpw  4508  onun2  4522  onuni  4526  elirr  4573  en2lp  4586  wetriext  4609  peano2  4627  relop  4812  elres  4978  sotri2  5063  iota4an  5235  iota5  5236  funeu  5279  funopg  5288  imadiflem  5333  funimaexglem  5337  ssimaex  5618  ffvelcdm  5691  dff3im  5703  dffo4  5706  f1eqcocnv  5834  f1oiso2  5870  riota5f  5898  riotass2  5900  acexmidlemcase  5913  ovmpodf  6050  ovmpodv2  6052  ovi3  6055  ov6g  6056  caoftrn  6158  op1steq  6232  tfr0dm  6375  tfrlemibxssdm  6380  tfrlemi14d  6386  tfr1onlembxssdm  6396  tfr1onlemaccex  6401  tfr1onlemres  6402  tfrcllembxssdm  6409  tfrcllemaccex  6414  tfrcllemres  6415  rdgivallem  6434  nnsucelsuc  6544  nnsucsssuc  6545  dcdifsnid  6557  nnawordex  6582  ersym  6599  mapvalg  6712  pmvalg  6713  mapsn  6744  fundmen  6860  pw2f1odclem  6890  mapdom1g  6903  fidceq  6925  fin0or  6942  findcard2  6945  findcard2s  6946  fiintim  6985  suplub2ti  7060  supsnti  7064  supisoex  7068  difinfsnlem  7158  difinfsn  7159  ctm  7168  ctssdclemn0  7169  ctssdccl  7170  ctssdc  7172  enumctlemm  7173  nninfninc  7182  nnnninfeq2  7188  enomnilem  7197  exmidomniim  7200  exmidomni  7201  fodjuomnilemdc  7203  fodjuomnilemres  7207  omnimkv  7215  mkvprop  7217  omniwomnimkv  7226  en2eleq  7255  acfun  7267  exmidontriimlem1  7281  exmidontriimlem4  7284  exmidontriim  7285  ccfunen  7324  cc4f  7329  cc4n  7331  elni2  7374  mulclpi  7388  nlt1pig  7401  indpi  7402  recclnq  7452  ltexnqq  7468  halfnqq  7470  prarloclemarch  7478  prarloclemarch2  7479  prop  7535  prltlu  7547  prarloclem3step  7556  prarloclem5  7560  prarloclem  7561  prarloc  7563  prarloc2  7564  genpml  7577  genpmu  7578  genprndl  7581  genprndu  7582  genpdisj  7583  addnqprllem  7587  addnqprulem  7588  addlocprlemeq  7593  addlocprlemgt  7594  addlocprlem  7595  addlocpr  7596  nqprloc  7605  nqprl  7611  nqpru  7612  addnqprlemrl  7617  addnqprlemru  7618  appdivnq  7623  prmuloc  7626  prmuloc2  7627  mullocprlem  7630  mullocpr  7631  mulnqprlemrl  7633  mulnqprlemru  7634  ltprordil  7649  ltpopr  7655  ltsopr  7656  ltaddpr  7657  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  ltexprlemloc  7667  ltexprlemfl  7669  ltexprlemrl  7670  ltexprlemfu  7671  ltexprlemru  7672  ltaprg  7679  recexprlemm  7684  recexprlem1ssl  7693  recexprlem1ssu  7694  aptiprleml  7699  aptiprlemu  7700  archpr  7703  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemupu  7709  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  cauappcvgprlem1  7719  archrecpr  7724  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemupu  7732  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemladdfu  7737  caucvgprlem1  7739  caucvgprlemlim  7741  caucvgprprlemnbj  7753  caucvgprprlemml  7754  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemupu  7760  caucvgprprlemdisj  7762  caucvgprprlemloc  7763  caucvgprprlemexbt  7766  caucvgprprlemaddq  7768  caucvgprprlemlim  7771  suplocexprlemss  7775  suplocexprlemrl  7777  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  suplocexprlemlub  7784  recexgt0sr  7833  mulgt0sr  7838  archsr  7842  caucvgsrlemoffcau  7858  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  cnm  7892  axarch  7951  axcaucvglemcau  7958  axpre-suploclemres  7961  lelttr  8108  ltletr  8109  ltled  8138  cnegexlem1  8194  cnegexlem2  8195  renegcl  8280  negf1o  8401  gt0add  8592  apreap  8606  apirr  8624  apsym  8625  apcotr  8626  apadd1  8627  apneg  8630  mulext1  8631  mulap0r  8634  apti  8641  aprcl  8665  aptap  8669  recexap  8672  mulap0  8673  receuap  8688  mul0eqap  8689  lep1  8864  lem1  8866  letrp1  8867  recreclt  8919  lbinf  8967  suprubex  8970  nnrecgt0  9020  bndndx  9239  nn0ge2m1nn  9300  elnn0z  9330  peano2z  9353  zaddcl  9357  ztri3or0  9359  zltnle  9363  zdceq  9392  zdcle  9393  zdclt  9394  zdiv  9405  zeo  9422  fnn0ind  9433  btwnz  9436  uzm1  9623  uzp1  9626  indstr  9658  supinfneg  9660  infsupneg  9661  eluzdc  9675  nn01to3  9682  qapne  9704  xrltled  9865  xrlelttr  9872  xrltletr  9873  ge0nemnf  9890  fzdcel  10106  elfzouz2  10228  fzoss1  10238  fzospliti  10243  fzocatel  10266  fzostep1  10304  qtri3or  10310  qltnle  10313  qdceq  10314  qdclt  10315  exbtwnzlemex  10318  rebtwn2zlemstep  10321  rebtwn2z  10323  qbtwnxr  10326  ioom  10329  ico0  10330  ioc0  10331  flqeqceilz  10389  modqadd1  10432  modqmul1  10448  frec2uzuzd  10473  frec2uzlt2d  10475  frec2uzf1od  10477  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgdomlem  10488  uzsinds  10515  seqvalcd  10532  seqovcd  10538  seq3fveq2  10546  seqfveq2g  10548  seq3shft2  10552  seqshft2g  10553  monoord  10556  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  iseqf1olemab  10573  iseqf1olemnanb  10574  iseqf1olemqk  10578  seqf1oglem1  10590  seqf1og  10592  seq3id3  10595  seq3id2  10597  seq3homo  10598  seqhomog  10601  expgt1  10648  m1expeven  10657  expnbnd  10734  expnlbnd2  10736  nn0ltexp2  10780  apexp1  10789  hashennn  10851  zfz1isolem1  10911  seq3coll  10913  cjap  11050  caucvgre  11125  cvg1nlemres  11129  resqrexlemgt0  11164  resqrexlemglsq  11166  resqrexlemga  11167  resqrtcl  11173  abslt  11232  abssubap0  11234  abssubne0  11235  caubnd2  11261  qdenre  11346  maxabslemlub  11351  maxabs  11353  maxleast  11357  fimaxre2  11370  xrmaxiflemlub  11391  xrmaxif  11394  xrmaxltsup  11401  xrmaxadd  11404  xrmineqinf  11412  climuni  11436  2clim  11444  climcn1  11451  climcn2  11452  subcn2  11454  mulcn2  11455  climsqz  11478  climsqz2  11479  climcau  11490  climcvg1nlem  11492  climcaucn  11494  serf0  11495  sumrbdclem  11520  summodclem2  11525  zsumdc  11527  divcnv  11640  absltap  11652  absgtap  11653  mertenslem2  11679  ntrivcvgap  11691  prodrbdclem  11714  prodmodclem2  11720  zproddc  11722  prodssdc  11732  fprodsplitdc  11739  fprodcl2lem  11748  efcllemp  11801  tanvalap  11851  sin01bnd  11900  cos01bnd  11901  sin01gt0  11905  absef  11913  eirrap  11921  dvds0  11949  dvdsmul1  11956  dvdsmultr1d  11975  dvdslelemd  11985  divconjdvds  11991  alzdvds  11996  sqoddm1div8z  12027  nno  12047  divalglemex  12063  zsupcllemstep  12082  zsupcl  12084  infssuzledc  12087  dvdsbnd  12093  dvdslegcd  12101  zeqzmulgcd  12107  gcd0id  12116  gcdaddm  12121  gcd1  12124  gcdabs  12125  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlemex  12138  bezoutlemzz  12139  bezoutlemaz  12140  bezoutlembz  12141  bezoutlembi  12142  bezoutlemle  12145  bezoutlemsup  12146  mulgcd  12153  gcdzeq  12159  dvdsmulgcd  12162  sqgcd  12166  bezoutr1  12170  nninfctlemfo  12177  algcvga  12189  algfx  12190  eucalglt  12195  eucalg  12197  lcmneg  12212  lcmabs  12214  lcmgcdlem  12215  ncoprmgcdne1b  12227  mulgcddvds  12232  qredeq  12234  divgcdcoprm0  12239  cncongr1  12241  isprm2lem  12254  nprm  12261  dvdsnprmd  12263  prmdvdsfz  12277  isprm5lem  12279  coprm  12282  isprm6  12285  sqrt2irr  12300  pw2dvdslemn  12303  pw2dvdseulemle  12305  oddpwdclemdvds  12308  oddpwdclemndvds  12309  sqrt2irrap  12318  qnumdencl  12325  prmdiv  12373  modprmn0modprm0  12394  prm23lt5  12401  pythagtriplem4  12406  pythagtriplem19  12420  pythagtrip  12421  pclemub  12425  pcpre1  12430  pcpremul  12431  pceulem  12432  pcqcl  12444  pcidlem  12461  pcgcd1  12466  pc2dvds  12468  dvdsprmpweqle  12475  difsqpwdvds  12476  pcadd  12478  pcmpt  12481  expnprm  12491  pockthg  12495  infpnlem2  12498  prmunb  12500  1arith  12505  4sqlem10  12525  4sqlem11  12539  4sqlem12  12540  4sqlem13m  12541  4sqlem17  12545  4sqlem18  12546  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemrnh  12573  ennnfonelemnn0  12579  ennnfonelemim  12581  exmidunben  12583  ctinfomlemom  12584  ctinfom  12585  ctinf  12587  omctfn  12600  nninfdclemp1  12607  setscomd  12659  imasaddfnlemg  12897  mhmf1o  13042  grpinveu  13110  grpasscan1  13135  dfgrp3mlem  13170  grp1inv  13179  issubg4m  13263  ghmf1o  13345  srgisid  13482  ringadd2  13523  ringinvnzdiv  13546  unitgrp  13612  ringelnzr  13683  lringuplu  13692  subrguss  13732  subrgintm  13739  aprcotr  13781  islmodd  13789  lssclg  13860  lss0cl  13865  lssvneln0  13869  lss1d  13879  lmodindp1  13924  rnglidlmmgm  13992  znidomb  14146  znunit  14147  znrrg  14148  tgcl  14232  neii1  14315  neii2  14317  neiss  14318  tpnei  14328  tgrest  14337  ssrest  14350  icnpimaex  14379  lmcvg  14385  cnpnei  14387  cnptopco  14390  lmff  14417  txcnp  14439  txcn  14443  hmeontr  14481  blssec  14606  mopni3  14652  blsscls2  14661  comet  14667  bdxmet  14669  bdmopn  14672  xmettxlem  14677  xmettx  14678  addcncntoplem  14719  mulc1cncf  14744  cncfco  14746  cncfmptc  14750  mulcncflem  14761  mulcncf  14762  dedekindeulemlu  14775  dedekindeulemeu  14776  suplociccreex  14778  suplociccex  14779  dedekindicclemlu  14784  dedekindicclemeu  14785  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemloc  14795  ivthinc  14797  ivthreinc  14799  ivthdichlem  14805  limcimolemlt  14818  limcresi  14820  cnplimcim  14821  cnplimclemle  14822  cnplimclemr  14823  limccnpcntop  14829  limccoap  14832  dvcoapbr  14856  dvcj  14858  plyf  14883  plyaddlem1  14893  plymullem1  14894  efltlemlt  14909  sin0pilem2  14917  tangtx  14973  logdivlti  15016  rplogbval  15077  logbgcd1irraplemexp  15100  logbgcd1irraplemap  15101  logbgcd1irrap  15102  lgsval4a  15138  lgsdir2lem3  15146  lgsne0  15154  gausslemma2dlem3  15179  gausslemma2dlem4  15180  gausslemma2dlem6  15183  gausslemma2dlem7  15184  gausslemma2d  15185  lgseisenlem1  15186  2lgsoddprmlem2  15194  2sqlem8a  15209  2sqlem8  15210  2sqlem9  15211  bj-exlimmpi  15262  uzdcinzz  15290  bj-charfundcALT  15301  bj-2inf  15430  bj-peano4  15447  bj-nn0suc  15456  1dom1el  15483  subctctexmid  15491  nninfalllem1  15498  nninfsellemqall  15505  nninfomnilem  15508  nninffeq  15510  exmidsbthrlem  15512  sbthomlem  15515  refeq  15518  isomninnlem  15520  apdifflemr  15537  redcwlpo  15545  reap0  15548  nconstwlpolem  15555