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  625  mt2d  630  mpnanrd  700  mpjaod  726  stdcndcOLD  854  impidc  866  jadc  871  pm2.54dc  899  oplem1  984  mp3and  1377  xor3dc  1432  exlimdd  1921  exlimddv  1950  eqrdav  2233  necon1aidc  2465  necon1bidc  2466  necon4aidc  2482  reximddv  2647  reximssdv  2648  rexlimddv  2667  vtoclgft  2867  rspcedvd  2929  sseldd  3243  ssneldd  3245  tpid3g  3812  preq12b  3879  axpweq  4289  exmid1dc  4318  exmid1stab  4326  opth  4358  issod  4445  frirrg  4476  frind  4478  ralxfr2d  4590  rexxfr2d  4591  eldifpw  4603  onun2  4617  onuni  4621  elirr  4668  en2lp  4681  wetriext  4704  peano2  4722  relop  4910  elres  5079  sotri2  5165  iota4an  5338  iota5  5339  funeu  5382  funopg  5391  imadiflem  5440  funimaexglem  5444  ssimaex  5743  ffvelcdm  5815  dff3im  5827  dffo4  5830  funopsn  5865  f1eqcocnv  5970  f1oiso2  6006  riota5f  6038  riotass2  6040  acexmidlemcase  6053  elovimad  6102  ovmpodf  6193  ovmpodv2  6195  ovi3  6199  ov6g  6200  caoftrn  6308  op1steq  6386  fvdifsuppst  6457  suppssdc  6473  suppofss1dcl  6477  suppofss2dcl  6478  tfr0dm  6566  tfrlemibxssdm  6571  tfrlemi14d  6577  tfr1onlembxssdm  6587  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllembxssdm  6600  tfrcllemaccex  6605  tfrcllemres  6606  rdgivallem  6625  nnsucelsuc  6737  nnsucsssuc  6738  dcdifsnid  6750  nnawordex  6775  ersym  6792  mapvalg  6905  pmvalg  6906  mapsnd  6936  mapsn  6938  fundmen  7060  1dom1el  7073  en2  7078  pw2f1odclem  7100  mapdom1g  7113  fidceq  7137  fin0or  7156  findcard2  7159  findcard2s  7160  fidcen  7169  prfidceq  7201  fiintim  7204  suplub2ti  7305  supsnti  7309  supisoex  7313  difinfsnlem  7403  difinfsn  7404  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  nninfninc  7427  nnnninfeq2  7433  enomnilem  7442  exmidomniim  7445  exmidomni  7446  fodjuomnilemdc  7448  fodjuomnilemres  7452  omnimkv  7460  mkvprop  7462  omniwomnimkv  7471  en2prde  7503  pr2cv1  7505  en2eleq  7511  acfun  7527  exmidontriimlem1  7541  exmidontriimlem4  7544  exmidontriim  7545  papsym  7576  papcotr  7577  ccfunen  7594  cc4f  7599  cc4n  7601  elni2  7645  mulclpi  7659  nlt1pig  7672  indpi  7673  recclnq  7723  ltexnqq  7739  halfnqq  7741  prarloclemarch  7749  prarloclemarch2  7750  prop  7806  prltlu  7818  prarloclem3step  7827  prarloclem5  7831  prarloclem  7832  prarloc  7834  prarloc2  7835  genpml  7848  genpmu  7849  genprndl  7852  genprndu  7853  genpdisj  7854  addnqprllem  7858  addnqprulem  7859  addlocprlemeq  7864  addlocprlemgt  7865  addlocprlem  7866  addlocpr  7867  nqprloc  7876  nqprl  7882  nqpru  7883  addnqprlemrl  7888  addnqprlemru  7889  appdivnq  7894  prmuloc  7897  prmuloc2  7898  mullocprlem  7901  mullocpr  7902  mulnqprlemrl  7904  mulnqprlemru  7905  ltprordil  7920  ltpopr  7926  ltsopr  7927  ltaddpr  7928  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemloc  7938  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  ltaprg  7950  recexprlemm  7955  recexprlem1ssl  7964  recexprlem1ssu  7965  aptiprleml  7970  aptiprlemu  7971  archpr  7974  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlem1  7990  archrecpr  7995  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlem1  8010  caucvgprlemlim  8012  caucvgprprlemnbj  8024  caucvgprprlemml  8025  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemupu  8031  caucvgprprlemdisj  8033  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  caucvgprprlemlim  8042  suplocexprlemss  8046  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  recexgt0sr  8104  mulgt0sr  8109  archsr  8113  caucvgsrlemoffcau  8129  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  cnm  8163  axarch  8222  axcaucvglemcau  8229  axpre-suploclemres  8232  lelttr  8378  ltletr  8379  ltled  8408  cnegexlem1  8464  cnegexlem2  8465  renegcl  8550  negf1o  8672  gt0add  8864  apreap  8878  apirr  8896  apsym  8897  apcotr  8898  apadd1  8899  apneg  8902  mulext1  8903  mulap0r  8906  apti  8913  aprcl  8937  aptap  8941  recexap  8944  mulap0  8945  receuap  8960  mul0eqap  8961  lep1  9136  lem1  9138  letrp1  9139  recreclt  9191  lbinf  9239  suprubex  9242  nnrecgt0  9292  bndndx  9512  nn0ge2m1nn  9577  elnn0z  9607  peano2z  9630  zaddcl  9634  ztri3or0  9636  zltnle  9640  zdceq  9670  zdcle  9671  zdclt  9672  zdiv  9684  zeo  9701  fnn0ind  9712  btwnz  9715  uzm1  9903  uzp1  9906  indstr  9943  supinfneg  9945  infsupneg  9946  eluzdc  9960  nn01to3  9967  qapne  9989  xrltled  10151  xrlelttr  10158  xrltletr  10159  ge0nemnf  10176  fzdcel  10394  elfzouz2  10518  fzoss1  10529  fzospliti  10534  elincfzoext  10560  fzocatel  10566  fzostep1  10605  zsupcllemstep  10611  zsupcl  10613  infssuzledc  10616  qtri3or  10624  qltnle  10627  qdceq  10628  qdclt  10629  exbtwnzlemex  10633  rebtwn2zlemstep  10636  rebtwn2z  10638  qbtwnxr  10641  ioom  10644  ico0  10645  ioc0  10646  flqeqceilz  10704  modqadd1  10747  modqmul1  10763  frec2uzuzd  10788  frec2uzlt2d  10790  frec2uzf1od  10792  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgdomlem  10803  uzsinds  10830  seqvalcd  10847  seqovcd  10853  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord  10871  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  iseqf1olemab  10888  iseqf1olemnanb  10889  iseqf1olemqk  10893  seqf1oglem1  10905  seqf1og  10907  seq3id3  10910  seq3id2  10912  seq3homo  10913  seqhomog  10916  expgt1  10963  m1expeven  10972  expnbnd  11050  expnlbnd2  11052  nn0ltexp2  11096  apexp1  11105  hashennn  11168  hashfibclem  11231  zfz1isolem1  11237  seq3coll  11239  pfxwrdsymbg  11407  wrdind  11439  wrd2ind  11440  cjap  11616  caucvgre  11691  cvg1nlemres  11695  resqrexlemgt0  11730  resqrexlemglsq  11732  resqrexlemga  11733  resqrtcl  11739  abslt  11798  abssubap0  11800  abssubne0  11801  caubnd2  11827  qdenre  11912  maxabslemlub  11917  maxabs  11919  maxleast  11923  fimaxre2  11937  xrmaxiflemlub  11958  xrmaxif  11961  xrmaxltsup  11968  xrmaxadd  11971  xrmineqinf  11979  climuni  12003  2clim  12011  climcn1  12018  climcn2  12019  subcn2  12021  mulcn2  12022  climsqz  12045  climsqz2  12046  climcau  12057  climcvg1nlem  12059  climcaucn  12061  serf0  12062  sumrbdclem  12088  summodclem2  12093  zsumdc  12095  divcnv  12208  absltap  12220  absgtap  12221  mertenslem2  12247  ntrivcvgap  12259  prodrbdclem  12282  prodmodclem2  12288  zproddc  12290  prodssdc  12300  fprodsplitdc  12307  fprodcl2lem  12316  efcllemp  12369  tanvalap  12419  sin01bnd  12468  cos01bnd  12469  sin01gt0  12473  absef  12481  eirrap  12489  dvds0  12517  dvdsmul1  12524  dvdsmultr1d  12543  dvdslelemd  12554  divconjdvds  12560  alzdvds  12565  3dvds  12575  sqoddm1div8z  12597  nno  12617  divalglemex  12633  bits0o  12661  dvdsbnd  12677  dvdslegcd  12685  zeqzmulgcd  12691  gcd0id  12700  gcdaddm  12705  gcd1  12708  gcdabs  12709  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlemex  12722  bezoutlemzz  12723  bezoutlemaz  12724  bezoutlembz  12725  bezoutlembi  12726  bezoutlemle  12729  bezoutlemsup  12730  mulgcd  12737  gcdzeq  12743  dvdsmulgcd  12746  sqgcd  12750  bezoutr1  12754  nninfctlemfo  12761  algcvga  12773  algfx  12774  eucalglt  12779  eucalg  12781  lcmneg  12796  lcmabs  12798  lcmgcdlem  12799  ncoprmgcdne1b  12811  mulgcddvds  12816  qredeq  12818  divgcdcoprm0  12823  cncongr1  12825  isprm2lem  12838  nprm  12845  dvdsnprmd  12847  prmdvdsfz  12861  isprm5lem  12863  coprm  12866  isprm6  12869  sqrt2irr  12884  pw2dvdslemn  12887  pw2dvdseulemle  12889  oddpwdclemdvds  12892  oddpwdclemndvds  12893  sqrt2irrap  12902  qnumdencl  12909  prmdiv  12957  modprmn0modprm0  12979  prm23lt5  12986  pythagtriplem4  12991  pythagtriplem19  13005  pythagtrip  13006  pclemub  13010  pcpre1  13015  pcpremul  13016  pceulem  13017  pcqcl  13029  pcidlem  13046  pcgcd1  13051  pc2dvds  13053  dvdsprmpweqle  13060  difsqpwdvds  13061  pcadd  13063  pcmpt  13066  expnprm  13076  pockthg  13080  infpnlem2  13083  prmunb  13085  1arith  13090  4sqlem10  13110  4sqlem11  13124  4sqlem12  13125  4sqlem13m  13126  4sqlem17  13130  4sqlem18  13131  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfrceq  13216  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemrnh  13251  ennnfonelemnn0  13257  ennnfonelemim  13259  exmidunben  13261  ctinfomlemom  13262  ctinfom  13263  ctinf  13265  omctfn  13278  nninfdclemp1  13285  setscomd  13337  imasaddfnlemg  13611  mhmf1o  13767  grpinveu  13835  grpasscan1  13860  dfgrp3mlem  13895  grp1inv  13904  issubg4m  13994  ghmf1o  14076  srgisid  14214  ringadd2  14255  ringinvnzdiv  14278  unitgrp  14346  ringelnzr  14417  lringuplu  14426  subrguss  14467  subrgintm  14474  aprcotr  14520  islmodd  14553  lssclg  14624  lss0cl  14629  lssvneln0  14633  lss1d  14643  lmodindp1  14688  rnglidlmmgm  14756  znidomb  14918  znunit  14919  znrrg  14920  mplsubgfilemcl  14966  mplsubgfileminv  14967  tgcl  15041  neii1  15124  neii2  15126  neiss  15127  tpnei  15137  tgrest  15146  ssrest  15159  icnpimaex  15188  lmcvg  15194  cnpnei  15196  cnptopco  15199  lmff  15226  txcnp  15248  txcn  15252  hmeontr  15290  blssec  15415  mopni3  15461  blsscls2  15470  comet  15476  bdxmet  15478  bdmopn  15481  xmettxlem  15486  xmettx  15487  addcncntoplem  15538  mpomulcn  15543  mulc1cncf  15566  cncfco  15568  cncfmptc  15573  mulcncflem  15584  mulcncf  15585  dedekindeulemlu  15598  dedekindeulemeu  15599  suplociccreex  15601  suplociccex  15602  dedekindicclemlu  15607  dedekindicclemeu  15608  ivthinclemlopn  15613  ivthinclemlr  15614  ivthinclemuopn  15615  ivthinclemur  15616  ivthinclemloc  15618  ivthinc  15620  ivthreinc  15622  ivthdichlem  15628  limcimolemlt  15641  limcresi  15643  cnplimcim  15644  cnplimclemle  15645  cnplimclemr  15646  limccnpcntop  15652  limccoap  15655  dvcoapbr  15684  dvcj  15686  plyf  15714  plyaddlem1  15724  plymullem1  15725  plyco  15736  plycj  15738  plycn  15739  plyrecj  15740  dvply2g  15743  efltlemlt  15751  sin0pilem2  15759  tangtx  15815  logdivlti  15858  rplogbval  15922  logbgcd1irraplemexp  15945  logbgcd1irraplemap  15946  logbgcd1irrap  15947  perfect1  15978  perfectlem1  15979  perfectlem2  15980  lgsval4a  16007  lgsdir2lem3  16015  lgsne0  16023  gausslemma2dlem3  16048  gausslemma2dlem4  16049  gausslemma2dlem6  16052  gausslemma2dlem7  16053  gausslemma2d  16054  lgseisenlem1  16055  lgsquadlem2  16063  lgsquadlem3  16064  lgsquad2lem2  16067  lgsquad3  16069  2lgsoddprmlem2  16091  2sqlem8a  16107  2sqlem8  16108  2sqlem9  16109  lpvtx  16186  upgrex  16210  upgr1een  16231  edgupgren  16248  umgredg  16252  upgrpredgv  16253  upgredg2vtx  16255  upgredgpr  16256  uspgrf1oedg  16283  usgredg4  16322  uspgredgdomord  16336  usgr1vr  16355  wlkvtxiedg  16452  wlkvtxiedgg  16453  wlk1walkdom  16466  upgriswlkdc  16467  upgrwlkedg  16468  uspgr2wlkeq  16472  uspgr2wlkeqi  16474  umgrwlknloop  16475  eupth2lem2dc  16566  trlsegvdeglem1  16567  eupth2lem3lem4fi  16580  bj-exlimmpi  16654  uzdcinzz  16682  bj-charfundcALT  16691  bj-2inf  16820  bj-peano4  16837  bj-nn0suc  16846  pw1ndom3  16876  subctctexmid  16886  exmidcon  16892  nninfalllem1  16898  nninfsellemqall  16905  nninfomnilem  16908  nninffeq  16910  nnnninfex  16912  exmidsbthrlem  16914  sbthomlem  16917  refeq  16920  isomninnlem  16926  apdifflemr  16943  redcwlpo  16952  reap0  16955  nconstwlpolem  16963