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  623  mt2d  628  mpnanrd  697  mpjaod  723  stdcndcOLD  851  impidc  863  jadc  868  pm2.54dc  896  oplem1  981  mp3and  1374  xor3dc  1429  exlimdd  1918  exlimddv  1945  eqrdav  2228  necon1aidc  2451  necon1bidc  2452  necon4aidc  2468  reximddv  2633  reximssdv  2634  rexlimddv  2653  vtoclgft  2851  rspcedvd  2913  sseldd  3225  ssneldd  3227  tpid3g  3782  preq12b  3848  axpweq  4255  exmid1dc  4284  exmid1stab  4292  opth  4323  issod  4410  frirrg  4441  frind  4443  ralxfr2d  4555  rexxfr2d  4556  eldifpw  4568  onun2  4582  onuni  4586  elirr  4633  en2lp  4646  wetriext  4669  peano2  4687  relop  4872  elres  5041  sotri2  5126  iota4an  5299  iota5  5300  funeu  5343  funopg  5352  imadiflem  5400  funimaexglem  5404  ssimaex  5697  ffvelcdm  5770  dff3im  5782  dffo4  5785  funopsn  5819  f1eqcocnv  5921  f1oiso2  5957  riota5f  5987  riotass2  5989  acexmidlemcase  6002  elovimad  6051  ovmpodf  6142  ovmpodv2  6144  ovi3  6148  ov6g  6149  caoftrn  6257  op1steq  6331  tfr0dm  6474  tfrlemibxssdm  6479  tfrlemi14d  6485  tfr1onlembxssdm  6495  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllembxssdm  6508  tfrcllemaccex  6513  tfrcllemres  6514  rdgivallem  6533  nnsucelsuc  6645  nnsucsssuc  6646  dcdifsnid  6658  nnawordex  6683  ersym  6700  mapvalg  6813  pmvalg  6814  mapsn  6845  fundmen  6967  en2  6981  pw2f1odclem  7003  mapdom1g  7016  fidceq  7039  fin0or  7056  findcard2  7059  findcard2s  7060  prfidceq  7098  fiintim  7101  suplub2ti  7176  supsnti  7180  supisoex  7184  difinfsnlem  7274  difinfsn  7275  ctm  7284  ctssdclemn0  7285  ctssdccl  7286  ctssdc  7288  enumctlemm  7289  nninfninc  7298  nnnninfeq2  7304  enomnilem  7313  exmidomniim  7316  exmidomni  7317  fodjuomnilemdc  7319  fodjuomnilemres  7323  omnimkv  7331  mkvprop  7333  omniwomnimkv  7342  en2prde  7374  pr2cv1  7376  en2eleq  7381  acfun  7397  exmidontriimlem1  7411  exmidontriimlem4  7414  exmidontriim  7415  ccfunen  7458  cc4f  7463  cc4n  7465  elni2  7509  mulclpi  7523  nlt1pig  7536  indpi  7537  recclnq  7587  ltexnqq  7603  halfnqq  7605  prarloclemarch  7613  prarloclemarch2  7614  prop  7670  prltlu  7682  prarloclem3step  7691  prarloclem5  7695  prarloclem  7696  prarloc  7698  prarloc2  7699  genpml  7712  genpmu  7713  genprndl  7716  genprndu  7717  genpdisj  7718  addnqprllem  7722  addnqprulem  7723  addlocprlemeq  7728  addlocprlemgt  7729  addlocprlem  7730  addlocpr  7731  nqprloc  7740  nqprl  7746  nqpru  7747  addnqprlemrl  7752  addnqprlemru  7753  appdivnq  7758  prmuloc  7761  prmuloc2  7762  mullocprlem  7765  mullocpr  7766  mulnqprlemrl  7768  mulnqprlemru  7769  ltprordil  7784  ltpopr  7790  ltsopr  7791  ltaddpr  7792  ltexprlemm  7795  ltexprlemopl  7796  ltexprlemlol  7797  ltexprlemopu  7798  ltexprlemupu  7799  ltexprlemloc  7802  ltexprlemfl  7804  ltexprlemrl  7805  ltexprlemfu  7806  ltexprlemru  7807  ltaprg  7814  recexprlemm  7819  recexprlem1ssl  7828  recexprlem1ssu  7829  aptiprleml  7834  aptiprlemu  7835  archpr  7838  cauappcvgprlemm  7840  cauappcvgprlemopl  7841  cauappcvgprlemlol  7842  cauappcvgprlemopu  7843  cauappcvgprlemupu  7844  cauappcvgprlemdisj  7846  cauappcvgprlemloc  7847  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  cauappcvgprlemladdru  7851  cauappcvgprlem1  7854  archrecpr  7859  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprlemm  7863  caucvgprlemopl  7864  caucvgprlemlol  7865  caucvgprlemopu  7866  caucvgprlemupu  7867  caucvgprlemdisj  7869  caucvgprlemloc  7870  caucvgprlemladdfu  7872  caucvgprlem1  7874  caucvgprlemlim  7876  caucvgprprlemnbj  7888  caucvgprprlemml  7889  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemopu  7894  caucvgprprlemupu  7895  caucvgprprlemdisj  7897  caucvgprprlemloc  7898  caucvgprprlemexbt  7901  caucvgprprlemaddq  7903  caucvgprprlemlim  7906  suplocexprlemss  7910  suplocexprlemrl  7912  suplocexprlemmu  7913  suplocexprlemru  7914  suplocexprlemdisj  7915  suplocexprlemloc  7916  suplocexprlemub  7918  suplocexprlemlub  7919  recexgt0sr  7968  mulgt0sr  7973  archsr  7977  caucvgsrlemoffcau  7993  suplocsrlemb  8001  suplocsrlempr  8002  suplocsrlem  8003  cnm  8027  axarch  8086  axcaucvglemcau  8093  axpre-suploclemres  8096  lelttr  8243  ltletr  8244  ltled  8273  cnegexlem1  8329  cnegexlem2  8330  renegcl  8415  negf1o  8536  gt0add  8728  apreap  8742  apirr  8760  apsym  8761  apcotr  8762  apadd1  8763  apneg  8766  mulext1  8767  mulap0r  8770  apti  8777  aprcl  8801  aptap  8805  recexap  8808  mulap0  8809  receuap  8824  mul0eqap  8825  lep1  9000  lem1  9002  letrp1  9003  recreclt  9055  lbinf  9103  suprubex  9106  nnrecgt0  9156  bndndx  9376  nn0ge2m1nn  9437  elnn0z  9467  peano2z  9490  zaddcl  9494  ztri3or0  9496  zltnle  9500  zdceq  9530  zdcle  9531  zdclt  9532  zdiv  9543  zeo  9560  fnn0ind  9571  btwnz  9574  uzm1  9761  uzp1  9764  indstr  9796  supinfneg  9798  infsupneg  9799  eluzdc  9813  nn01to3  9820  qapne  9842  xrltled  10003  xrlelttr  10010  xrltletr  10011  ge0nemnf  10028  fzdcel  10244  elfzouz2  10366  fzoss1  10377  fzospliti  10382  elincfzoext  10407  fzocatel  10413  fzostep1  10451  zsupcllemstep  10457  zsupcl  10459  infssuzledc  10462  qtri3or  10468  qltnle  10471  qdceq  10472  qdclt  10473  exbtwnzlemex  10477  rebtwn2zlemstep  10480  rebtwn2z  10482  qbtwnxr  10485  ioom  10488  ico0  10489  ioc0  10490  flqeqceilz  10548  modqadd1  10591  modqmul1  10607  frec2uzuzd  10632  frec2uzlt2d  10634  frec2uzf1od  10636  frecuzrdgrrn  10638  frec2uzrdg  10639  frecuzrdgrcl  10640  frecuzrdgsuc  10644  frecuzrdgrclt  10645  frecuzrdgdomlem  10647  uzsinds  10674  seqvalcd  10691  seqovcd  10697  seq3fveq2  10705  seqfveq2g  10707  seq3shft2  10711  seqshft2g  10712  monoord  10715  seq3split  10718  seqsplitg  10719  seq3caopr3  10721  iseqf1olemab  10732  iseqf1olemnanb  10733  iseqf1olemqk  10737  seqf1oglem1  10749  seqf1og  10751  seq3id3  10754  seq3id2  10756  seq3homo  10757  seqhomog  10760  expgt1  10807  m1expeven  10816  expnbnd  10893  expnlbnd2  10895  nn0ltexp2  10939  apexp1  10948  hashennn  11010  zfz1isolem1  11070  seq3coll  11072  pfxwrdsymbg  11230  wrdind  11262  wrd2ind  11263  cjap  11425  caucvgre  11500  cvg1nlemres  11504  resqrexlemgt0  11539  resqrexlemglsq  11541  resqrexlemga  11542  resqrtcl  11548  abslt  11607  abssubap0  11609  abssubne0  11610  caubnd2  11636  qdenre  11721  maxabslemlub  11726  maxabs  11728  maxleast  11732  fimaxre2  11746  xrmaxiflemlub  11767  xrmaxif  11770  xrmaxltsup  11777  xrmaxadd  11780  xrmineqinf  11788  climuni  11812  2clim  11820  climcn1  11827  climcn2  11828  subcn2  11830  mulcn2  11831  climsqz  11854  climsqz2  11855  climcau  11866  climcvg1nlem  11868  climcaucn  11870  serf0  11871  sumrbdclem  11896  summodclem2  11901  zsumdc  11903  divcnv  12016  absltap  12028  absgtap  12029  mertenslem2  12055  ntrivcvgap  12067  prodrbdclem  12090  prodmodclem2  12096  zproddc  12098  prodssdc  12108  fprodsplitdc  12115  fprodcl2lem  12124  efcllemp  12177  tanvalap  12227  sin01bnd  12276  cos01bnd  12277  sin01gt0  12281  absef  12289  eirrap  12297  dvds0  12325  dvdsmul1  12332  dvdsmultr1d  12351  dvdslelemd  12362  divconjdvds  12368  alzdvds  12373  3dvds  12383  sqoddm1div8z  12405  nno  12425  divalglemex  12441  bits0o  12469  dvdsbnd  12485  dvdslegcd  12493  zeqzmulgcd  12499  gcd0id  12508  gcdaddm  12513  gcd1  12516  gcdabs  12517  bezoutlemnewy  12525  bezoutlemstep  12526  bezoutlemmain  12527  bezoutlemex  12530  bezoutlemzz  12531  bezoutlemaz  12532  bezoutlembz  12533  bezoutlembi  12534  bezoutlemle  12537  bezoutlemsup  12538  mulgcd  12545  gcdzeq  12551  dvdsmulgcd  12554  sqgcd  12558  bezoutr1  12562  nninfctlemfo  12569  algcvga  12581  algfx  12582  eucalglt  12587  eucalg  12589  lcmneg  12604  lcmabs  12606  lcmgcdlem  12607  ncoprmgcdne1b  12619  mulgcddvds  12624  qredeq  12626  divgcdcoprm0  12631  cncongr1  12633  isprm2lem  12646  nprm  12653  dvdsnprmd  12655  prmdvdsfz  12669  isprm5lem  12671  coprm  12674  isprm6  12677  sqrt2irr  12692  pw2dvdslemn  12695  pw2dvdseulemle  12697  oddpwdclemdvds  12700  oddpwdclemndvds  12701  sqrt2irrap  12710  qnumdencl  12717  prmdiv  12765  modprmn0modprm0  12787  prm23lt5  12794  pythagtriplem4  12799  pythagtriplem19  12813  pythagtrip  12814  pclemub  12818  pcpre1  12823  pcpremul  12824  pceulem  12825  pcqcl  12837  pcidlem  12854  pcgcd1  12859  pc2dvds  12861  dvdsprmpweqle  12868  difsqpwdvds  12869  pcadd  12871  pcmpt  12874  expnprm  12884  pockthg  12888  infpnlem2  12891  prmunb  12893  1arith  12898  4sqlem10  12918  4sqlem11  12932  4sqlem12  12933  4sqlem13m  12934  4sqlem17  12938  4sqlem18  12939  ennnfonelemex  12993  ennnfonelemhom  12994  ennnfonelemrnh  12995  ennnfonelemnn0  13001  ennnfonelemim  13003  exmidunben  13005  ctinfomlemom  13006  ctinfom  13007  ctinf  13009  omctfn  13022  nninfdclemp1  13029  setscomd  13081  imasaddfnlemg  13355  mhmf1o  13511  grpinveu  13579  grpasscan1  13604  dfgrp3mlem  13639  grp1inv  13648  issubg4m  13738  ghmf1o  13820  srgisid  13957  ringadd2  13998  ringinvnzdiv  14021  unitgrp  14088  ringelnzr  14159  lringuplu  14168  subrguss  14208  subrgintm  14215  aprcotr  14257  islmodd  14265  lssclg  14336  lss0cl  14341  lssvneln0  14345  lss1d  14355  lmodindp1  14400  rnglidlmmgm  14468  znidomb  14630  znunit  14631  znrrg  14632  mplsubgfilemcl  14671  mplsubgfileminv  14672  tgcl  14746  neii1  14829  neii2  14831  neiss  14832  tpnei  14842  tgrest  14851  ssrest  14864  icnpimaex  14893  lmcvg  14899  cnpnei  14901  cnptopco  14904  lmff  14931  txcnp  14953  txcn  14957  hmeontr  14995  blssec  15120  mopni3  15166  blsscls2  15175  comet  15181  bdxmet  15183  bdmopn  15186  xmettxlem  15191  xmettx  15192  addcncntoplem  15243  mpomulcn  15248  mulc1cncf  15271  cncfco  15273  cncfmptc  15278  mulcncflem  15289  mulcncf  15290  dedekindeulemlu  15303  dedekindeulemeu  15304  suplociccreex  15306  suplociccex  15307  dedekindicclemlu  15312  dedekindicclemeu  15313  ivthinclemlopn  15318  ivthinclemlr  15319  ivthinclemuopn  15320  ivthinclemur  15321  ivthinclemloc  15323  ivthinc  15325  ivthreinc  15327  ivthdichlem  15333  limcimolemlt  15346  limcresi  15348  cnplimcim  15349  cnplimclemle  15350  cnplimclemr  15351  limccnpcntop  15357  limccoap  15360  dvcoapbr  15389  dvcj  15391  plyf  15419  plyaddlem1  15429  plymullem1  15430  plyco  15441  plycj  15443  plycn  15444  plyrecj  15445  dvply2g  15448  efltlemlt  15456  sin0pilem2  15464  tangtx  15520  logdivlti  15563  rplogbval  15627  logbgcd1irraplemexp  15650  logbgcd1irraplemap  15651  logbgcd1irrap  15652  perfect1  15680  perfectlem1  15681  perfectlem2  15682  lgsval4a  15709  lgsdir2lem3  15717  lgsne0  15725  gausslemma2dlem3  15750  gausslemma2dlem4  15751  gausslemma2dlem6  15754  gausslemma2dlem7  15755  gausslemma2d  15756  lgseisenlem1  15757  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad2lem2  15769  lgsquad3  15771  2lgsoddprmlem2  15793  2sqlem8a  15809  2sqlem8  15810  2sqlem9  15811  lpvtx  15887  upgrex  15911  edgupgren  15947  umgredg  15951  upgrpredgv  15952  upgredg2vtx  15954  upgredgpr  15955  uspgrf1oedg  15982  usgredg4  16021  uspgredgdomord  16035  wlkvtxiedg  16066  wlkvtxiedgg  16067  wlk1walkdom  16080  upgriswlkdc  16081  upgrwlkedg  16082  uspgr2wlkeq  16086  uspgr2wlkeqi  16088  umgrwlknloop  16089  bj-exlimmpi  16158  uzdcinzz  16186  bj-charfundcALT  16196  bj-2inf  16325  bj-peano4  16342  bj-nn0suc  16351  1dom1el  16378  fidcen  16379  pw1ndom3  16383  subctctexmid  16395  nninfalllem1  16404  nninfsellemqall  16411  nninfomnilem  16414  nninffeq  16416  nnnninfex  16418  exmidsbthrlem  16420  sbthomlem  16423  refeq  16426  isomninnlem  16428  apdifflemr  16445  redcwlpo  16453  reap0  16456  nconstwlpolem  16463