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  620  mt2d  625  mpjaod  718  stdcndcOLD  846  impidc  858  jadc  863  pm2.54dc  891  pm4.55dc  938  oplem1  975  mp3and  1340  xor3dc  1387  exlimdd  1872  exlimddv  1898  eqrdav  2176  necon1aidc  2398  necon1bidc  2399  necon4aidc  2415  reximddv  2580  reximssdv  2581  rexlimddv  2599  vtoclgft  2789  rspcedvd  2849  sseldd  3158  ssneldd  3160  tpid3g  3709  preq12b  3772  axpweq  4173  exmid1dc  4202  exmid1stab  4210  opth  4239  issod  4321  frirrg  4352  frind  4354  ralxfr2d  4466  rexxfr2d  4467  eldifpw  4479  onun2  4491  onuni  4495  elirr  4542  en2lp  4555  wetriext  4578  peano2  4596  relop  4779  elres  4945  sotri2  5028  iota4an  5199  iota5  5200  funeu  5243  funopg  5252  imadiflem  5297  funimaexglem  5301  ssimaex  5580  ffvelcdm  5652  dff3im  5664  dffo4  5667  f1eqcocnv  5795  f1oiso2  5831  riota5f  5858  riotass2  5860  acexmidlemcase  5873  ovmpodf  6009  ovmpodv2  6011  ovi3  6014  ov6g  6015  caoftrn  6111  op1steq  6183  tfr0dm  6326  tfrlemibxssdm  6331  tfrlemi14d  6337  tfr1onlembxssdm  6347  tfr1onlemaccex  6352  tfr1onlemres  6353  tfrcllembxssdm  6360  tfrcllemaccex  6365  tfrcllemres  6366  rdgivallem  6385  nnsucelsuc  6495  nnsucsssuc  6496  dcdifsnid  6508  nnawordex  6533  ersym  6550  mapvalg  6661  pmvalg  6662  mapsn  6693  fundmen  6809  mapdom1g  6850  fidceq  6872  fin0or  6889  findcard2  6892  findcard2s  6893  fiintim  6931  suplub2ti  7003  supsnti  7007  supisoex  7011  difinfsnlem  7101  difinfsn  7102  ctm  7111  ctssdclemn0  7112  ctssdccl  7113  ctssdc  7115  enumctlemm  7116  nnnninfeq2  7130  enomnilem  7139  exmidomniim  7142  exmidomni  7143  fodjuomnilemdc  7145  fodjuomnilemres  7149  omnimkv  7157  mkvprop  7159  omniwomnimkv  7168  en2eleq  7197  acfun  7209  exmidontriimlem1  7223  exmidontriimlem4  7226  exmidontriim  7227  ccfunen  7266  cc4f  7271  cc4n  7273  elni2  7316  mulclpi  7330  nlt1pig  7343  indpi  7344  recclnq  7394  ltexnqq  7410  halfnqq  7412  prarloclemarch  7420  prarloclemarch2  7421  prop  7477  prltlu  7489  prarloclem3step  7498  prarloclem5  7502  prarloclem  7503  prarloc  7505  prarloc2  7506  genpml  7519  genpmu  7520  genprndl  7523  genprndu  7524  genpdisj  7525  addnqprllem  7529  addnqprulem  7530  addlocprlemeq  7535  addlocprlemgt  7536  addlocprlem  7537  addlocpr  7538  nqprloc  7547  nqprl  7553  nqpru  7554  addnqprlemrl  7559  addnqprlemru  7560  appdivnq  7565  prmuloc  7568  prmuloc2  7569  mullocprlem  7572  mullocpr  7573  mulnqprlemrl  7575  mulnqprlemru  7576  ltprordil  7591  ltpopr  7597  ltsopr  7598  ltaddpr  7599  ltexprlemm  7602  ltexprlemopl  7603  ltexprlemlol  7604  ltexprlemopu  7605  ltexprlemupu  7606  ltexprlemloc  7609  ltexprlemfl  7611  ltexprlemrl  7612  ltexprlemfu  7613  ltexprlemru  7614  ltaprg  7621  recexprlemm  7626  recexprlem1ssl  7635  recexprlem1ssu  7636  aptiprleml  7641  aptiprlemu  7642  archpr  7645  cauappcvgprlemm  7647  cauappcvgprlemopl  7648  cauappcvgprlemlol  7649  cauappcvgprlemopu  7650  cauappcvgprlemupu  7651  cauappcvgprlemdisj  7653  cauappcvgprlemloc  7654  cauappcvgprlemladdfu  7656  cauappcvgprlemladdfl  7657  cauappcvgprlemladdru  7658  cauappcvgprlem1  7661  archrecpr  7666  caucvgprlemnkj  7668  caucvgprlemnbj  7669  caucvgprlemm  7670  caucvgprlemopl  7671  caucvgprlemlol  7672  caucvgprlemopu  7673  caucvgprlemupu  7674  caucvgprlemdisj  7676  caucvgprlemloc  7677  caucvgprlemladdfu  7679  caucvgprlem1  7681  caucvgprlemlim  7683  caucvgprprlemnbj  7695  caucvgprprlemml  7696  caucvgprprlemopl  7699  caucvgprprlemlol  7700  caucvgprprlemopu  7701  caucvgprprlemupu  7702  caucvgprprlemdisj  7704  caucvgprprlemloc  7705  caucvgprprlemexbt  7708  caucvgprprlemaddq  7710  caucvgprprlemlim  7713  suplocexprlemss  7717  suplocexprlemrl  7719  suplocexprlemmu  7720  suplocexprlemru  7721  suplocexprlemdisj  7722  suplocexprlemloc  7723  suplocexprlemub  7725  suplocexprlemlub  7726  recexgt0sr  7775  mulgt0sr  7780  archsr  7784  caucvgsrlemoffcau  7800  suplocsrlemb  7808  suplocsrlempr  7809  suplocsrlem  7810  cnm  7834  axarch  7893  axcaucvglemcau  7900  axpre-suploclemres  7903  lelttr  8049  ltletr  8050  ltled  8079  cnegexlem1  8135  cnegexlem2  8136  renegcl  8221  negf1o  8342  gt0add  8533  apreap  8547  apirr  8565  apsym  8566  apcotr  8567  apadd1  8568  apneg  8571  mulext1  8572  mulap0r  8575  apti  8582  aprcl  8606  aptap  8610  recexap  8613  mulap0  8614  receuap  8629  mul0eqap  8630  lep1  8805  lem1  8807  letrp1  8808  recreclt  8860  lbinf  8908  suprubex  8911  nnrecgt0  8960  bndndx  9178  nn0ge2m1nn  9239  elnn0z  9269  peano2z  9292  zaddcl  9296  ztri3or0  9298  zltnle  9302  zdceq  9331  zdcle  9332  zdclt  9333  zdiv  9344  zeo  9361  fnn0ind  9372  btwnz  9375  uzm1  9561  uzp1  9564  indstr  9596  supinfneg  9598  infsupneg  9599  eluzdc  9613  nn01to3  9620  qapne  9642  xrltled  9802  xrlelttr  9809  xrltletr  9810  ge0nemnf  9827  fzdcel  10043  elfzouz2  10164  fzoss1  10174  fzospliti  10179  fzocatel  10202  fzostep1  10240  qtri3or  10246  qltnle  10249  qdceq  10250  exbtwnzlemex  10253  rebtwn2zlemstep  10256  rebtwn2z  10258  qbtwnxr  10261  ioom  10264  ico0  10265  ioc0  10266  flqeqceilz  10321  modqadd1  10364  modqmul1  10380  frec2uzuzd  10405  frec2uzlt2d  10407  frec2uzf1od  10409  frecuzrdgrrn  10411  frec2uzrdg  10412  frecuzrdgrcl  10413  frecuzrdgsuc  10417  frecuzrdgrclt  10418  frecuzrdgdomlem  10420  uzsinds  10445  seqvalcd  10462  seqovcd  10466  seq3fveq2  10472  seq3shft2  10476  monoord  10479  seq3split  10482  seq3caopr3  10484  iseqf1olemab  10492  iseqf1olemnanb  10493  iseqf1olemqk  10497  seq3id3  10510  seq3id2  10512  seq3homo  10513  expgt1  10561  m1expeven  10570  expnbnd  10647  expnlbnd2  10649  nn0ltexp2  10692  apexp1  10701  hashennn  10763  zfz1isolem1  10823  seq3coll  10825  cjap  10918  caucvgre  10993  cvg1nlemres  10997  resqrexlemgt0  11032  resqrexlemglsq  11034  resqrexlemga  11035  resqrtcl  11041  abslt  11100  abssubap0  11102  abssubne0  11103  caubnd2  11129  qdenre  11214  maxabslemlub  11219  maxabs  11221  maxleast  11225  fimaxre2  11238  xrmaxiflemlub  11259  xrmaxif  11262  xrmaxltsup  11269  xrmaxadd  11272  xrmineqinf  11280  climuni  11304  2clim  11312  climcn1  11319  climcn2  11320  subcn2  11322  mulcn2  11323  climsqz  11346  climsqz2  11347  climcau  11358  climcvg1nlem  11360  climcaucn  11362  serf0  11363  sumrbdclem  11388  summodclem2  11393  zsumdc  11395  divcnv  11508  absltap  11520  absgtap  11521  mertenslem2  11547  ntrivcvgap  11559  prodrbdclem  11582  prodmodclem2  11588  zproddc  11590  prodssdc  11600  fprodsplitdc  11607  fprodcl2lem  11616  efcllemp  11669  tanvalap  11719  sin01bnd  11768  cos01bnd  11769  sin01gt0  11772  absef  11780  eirrap  11788  dvds0  11816  dvdsmul1  11823  dvdsmultr1d  11842  dvdslelemd  11852  divconjdvds  11858  alzdvds  11863  sqoddm1div8z  11894  nno  11914  divalglemex  11930  zsupcllemstep  11949  zsupcl  11951  infssuzledc  11954  dvdsbnd  11960  dvdslegcd  11968  zeqzmulgcd  11974  gcd0id  11983  gcdaddm  11988  gcd1  11991  gcdabs  11992  bezoutlemnewy  12000  bezoutlemstep  12001  bezoutlemmain  12002  bezoutlemex  12005  bezoutlemzz  12006  bezoutlemaz  12007  bezoutlembz  12008  bezoutlembi  12009  bezoutlemle  12012  bezoutlemsup  12013  mulgcd  12020  gcdzeq  12026  dvdsmulgcd  12029  sqgcd  12033  bezoutr1  12037  algcvga  12054  algfx  12055  eucalglt  12060  eucalg  12062  lcmneg  12077  lcmabs  12079  lcmgcdlem  12080  ncoprmgcdne1b  12092  mulgcddvds  12097  qredeq  12099  divgcdcoprm0  12104  cncongr1  12106  isprm2lem  12119  nprm  12126  dvdsnprmd  12128  prmdvdsfz  12142  isprm5lem  12144  coprm  12147  isprm6  12150  sqrt2irr  12165  pw2dvdslemn  12168  pw2dvdseulemle  12170  oddpwdclemdvds  12173  oddpwdclemndvds  12174  sqrt2irrap  12183  qnumdencl  12190  prmdiv  12238  modprmn0modprm0  12259  prm23lt5  12266  pythagtriplem4  12271  pythagtriplem19  12285  pythagtrip  12286  pclemub  12290  pcpre1  12295  pcpremul  12296  pceulem  12297  pcqcl  12309  pcidlem  12325  pcgcd1  12330  pc2dvds  12332  dvdsprmpweqle  12339  difsqpwdvds  12340  pcadd  12342  pcmpt  12344  expnprm  12354  pockthg  12358  infpnlem2  12361  prmunb  12363  1arith  12368  4sqlem10  12388  ennnfonelemex  12418  ennnfonelemhom  12419  ennnfonelemrnh  12420  ennnfonelemnn0  12426  ennnfonelemim  12428  exmidunben  12430  ctinfomlemom  12431  ctinfom  12432  ctinf  12434  omctfn  12447  nninfdclemp1  12454  setscomd  12506  imasaddfnlemg  12741  mhmf1o  12867  grpinveu  12917  grpasscan1  12939  dfgrp3mlem  12974  grp1inv  12983  issubg4m  13059  srgisid  13175  ringadd2  13216  ringinvnzdiv  13233  unitgrp  13291  ringelnzr  13334  lringuplu  13343  subrguss  13363  subrgintm  13370  aprcotr  13381  islmodd  13389  lssclg  13457  lss0cl  13462  lssvneln0  13466  lss1d  13476  lmodindp1  13520  tgcl  13704  neii1  13787  neii2  13789  neiss  13790  tpnei  13800  tgrest  13809  ssrest  13822  icnpimaex  13851  lmcvg  13857  cnpnei  13859  cnptopco  13862  lmff  13889  txcnp  13911  txcn  13915  hmeontr  13953  blssec  14078  mopni3  14124  blsscls2  14133  comet  14139  bdxmet  14141  bdmopn  14144  xmettxlem  14149  xmettx  14150  addcncntoplem  14191  mulc1cncf  14216  cncfco  14218  cncfmptc  14222  mulcncflem  14230  mulcncf  14231  dedekindeulemlu  14239  dedekindeulemeu  14240  suplociccreex  14242  suplociccex  14243  dedekindicclemlu  14248  dedekindicclemeu  14249  ivthinclemlopn  14254  ivthinclemlr  14255  ivthinclemuopn  14256  ivthinclemur  14257  ivthinclemloc  14259  ivthinc  14261  limcimolemlt  14273  limcresi  14275  cnplimcim  14276  cnplimclemle  14277  cnplimclemr  14278  limccnpcntop  14284  limccoap  14287  dvcoapbr  14311  dvcj  14313  efltlemlt  14335  sin0pilem2  14343  tangtx  14399  logdivlti  14442  rplogbval  14503  logbgcd1irraplemexp  14526  logbgcd1irraplemap  14527  logbgcd1irrap  14528  lgsval4a  14563  lgsdir2lem3  14571  lgsne0  14579  lgseisenlem1  14590  2lgsoddprmlem2  14594  2sqlem8a  14609  2sqlem8  14610  2sqlem9  14611  bj-exlimmpi  14662  uzdcinzz  14690  bj-charfundcALT  14701  bj-2inf  14830  bj-peano4  14847  bj-nn0suc  14856  1dom1el  14883  subctctexmid  14891  nninfalllem1  14898  nninfsellemqall  14905  nninfomnilem  14908  nninffeq  14910  exmidsbthrlem  14911  sbthomlem  14914  refeq  14917  isomninnlem  14919  apdifflemr  14936  redcwlpo  14944  reap0  14947  nconstwlpolem  14954