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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-2 7

This theorem is used 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  437  pm2.21dd  629  mt2d  634  mpnanrd  704  mpjaod  730  stdcndcOLD  858  impidc  870  jadc  875  pm2.54dc  903  oplem1  988  mp3and  1381  xor3dc  1436  exlimdd  1925  exlimddv  1954  eqrdav  2237  necon1aidc  2471  necon1bidc  2472  necon4aidc  2488  reximddv  2653  reximssdv  2654  rexlimddv  2673  vtoclgft  2873  rspcedvd  2935  sseldd  3249  ssneldd  3251  tpid3g  3828  preq12b  3895  axpweq  4308  exmid1dc  4337  exmid1stab  4345  opth  4377  issod  4464  frirrg  4495  frind  4497  ralxfr2d  4610  rexxfr2d  4611  eldifpw  4623  onun2  4637  onuni  4641  elirr  4688  en2lp  4701  wetriext  4724  peano2  4742  relop  4930  elres  5099  sotri2  5185  iota4an  5358  iota5  5359  funeu  5402  funopg  5411  imadiflem  5460  funimaexglem  5464  ssimaex  5764  ffvelcdm  5841  dff3im  5853  dffo4  5856  funopsn  5891  f1eqcocnv  5997  f1oiso2  6033  riota5f  6065  riotass2  6067  acexmidlemcase  6080  elovimad  6129  ovmpodf  6220  ovmpodv2  6222  ovi3  6226  ov6g  6227  caoftrn  6335  op1steq  6413  fvdifsuppst  6484  suppssdc  6500  suppofss1dcl  6504  suppofss2dcl  6505  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemi14d  6604  tfr1onlembxssdm  6614  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllembxssdm  6627  tfrcllemaccex  6632  tfrcllemres  6633  rdgivallem  6652  nnsucelsuc  6764  nnsucsssuc  6765  dcdifsnid  6777  nnawordex  6802  ersym  6819  mapvalg  6932  pmvalg  6933  mapsnd  6970  mapsn  6972  fundmen  7094  1dom1el  7107  en2  7112  pw2f1odclem  7134  mapdom1g  7147  fidceq  7171  fin0or  7190  findcard2  7193  findcard2s  7194  fidcen  7203  prfidceq  7235  fiintim  7238  suplub2ti  7342  supsnti  7346  supisoex  7350  difinfsnlem  7440  difinfsn  7441  ctm  7450  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  enumctlemm  7455  nninfninc  7464  nnnninfeq2  7470  enomnilem  7479  exmidomniim  7482  exmidomni  7483  fodjuomnilemdc  7485  fodjuomnilemres  7489  omnimkv  7497  mkvprop  7499  omniwomnimkv  7508  en2prde  7540  pr2cv1  7542  en2eleq  7548  acfun  7564  exmidontriimlem1  7578  exmidontriimlem4  7581  exmidontriim  7582  papsym  7613  papcotr  7614  ccfunen  7631  cc4f  7636  cc4n  7638  elni2  7682  mulclpi  7696  nlt1pig  7709  indpi  7710  recclnq  7760  ltexnqq  7776  halfnqq  7778  prarloclemarch  7786  prarloclemarch2  7787  prop  7843  prltlu  7855  prarloclem3step  7864  prarloclem5  7868  prarloclem  7869  prarloc  7871  prarloc2  7872  genpml  7885  genpmu  7886  genprndl  7889  genprndu  7890  genpdisj  7891  addnqprllem  7895  addnqprulem  7896  addlocprlemeq  7901  addlocprlemgt  7902  addlocprlem  7903  addlocpr  7904  nqprloc  7913  nqprl  7919  nqpru  7920  addnqprlemrl  7925  addnqprlemru  7926  appdivnq  7931  prmuloc  7934  prmuloc2  7935  mullocprlem  7938  mullocpr  7939  mulnqprlemrl  7941  mulnqprlemru  7942  ltprordil  7957  ltpopr  7963  ltsopr  7964  ltaddpr  7965  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  ltaprg  7987  recexprlemm  7992  recexprlem1ssl  8001  recexprlem1ssu  8002  aptiprleml  8007  aptiprlemu  8008  archpr  8011  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlem1  8027  archrecpr  8032  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprlem1  8047  caucvgprlemlim  8049  caucvgprprlemnbj  8061  caucvgprprlemml  8062  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemupu  8068  caucvgprprlemdisj  8070  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  caucvgprprlemaddq  8076  caucvgprprlemlim  8079  suplocexprlemss  8083  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  recexgt0sr  8141  mulgt0sr  8146  archsr  8150  caucvgsrlemoffcau  8166  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  cnm  8200  axarch  8259  axcaucvglemcau  8266  axpre-suploclemres  8269  lelttr  8415  ltletr  8416  ltled  8447  cnegexlem1  8503  cnegexlem2  8504  renegcl  8589  negf1o  8711  gt0add  8904  apreap  8918  apirr  8936  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  mulap0r  8946  apti  8953  aprcl  8977  aptap  8981  recexap  8984  mulap0  8985  receuap  9002  mul0eqap  9003  lep1  9178  lem1  9180  letrp1  9181  recreclt  9233  lbinf  9281  suprubex  9284  nnrecgt0  9345  bndndx  9567  nn0ge2m1nn  9632  elnn0z  9662  peano2z  9685  zaddcl  9689  ztri3or0  9691  zltnle  9695  zdceq  9725  zdcle  9726  zdclt  9727  zdiv  9739  zeo  9756  fnn0ind  9767  btwnz  9770  uzm1  9963  uzp1  9966  indstr  10003  supinfneg  10005  infsupneg  10006  eluzdc  10020  nn01to3  10027  qapne  10049  xrltled  10212  xrlelttr  10219  xrltletr  10220  ge0nemnf  10237  fzdcel  10455  elfzouz2  10580  fzoss1  10591  fzospliti  10596  elincfzoext  10622  fzocatel  10628  fzostep1  10667  zsupcllemstep  10673  zsupcl  10675  infssuzledc  10678  qtri3or  10686  qltnle  10689  qdceq  10690  qdclt  10691  exbtwnzlemex  10695  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnxr  10703  ioom  10706  ico0  10707  ioc0  10708  flqeqceilz  10769  modqadd1  10812  modqmul1  10828  frec2uzuzd  10853  frec2uzlt2d  10855  frec2uzf1od  10857  frecuzrdgrrn  10859  frec2uzrdg  10860  frecuzrdgrcl  10861  frecuzrdgsuc  10865  frecuzrdgrclt  10866  frecuzrdgdomlem  10868  uzsinds  10895  seqvalcd  10912  seqovcd  10918  seq3fveq2  10926  seqfveq2g  10928  seq3shft2  10932  seqshft2g  10933  monoord  10936  seq3split  10939  seqsplitg  10940  seq3caopr3  10942  iseqf1olemab  10953  iseqf1olemnanb  10954  iseqf1olemqk  10958  seqf1oglem1  10970  seqf1og  10972  seq3id3  10975  seq3id2  10977  seq3homo  10978  seqhomog  10981  expgt1  11028  m1expeven  11037  expnbnd  11115  expnlbnd2  11117  nn0ltexp2  11162  apexp1  11171  hashennn  11234  hashfibclem  11297  hashf1lem2  11301  zfz1isolem1  11307  seq3coll  11309  pfxwrdsymbg  11477  wrdind  11509  wrd2ind  11510  cjap  11687  caucvgre  11762  cvg1nlemres  11766  resqrexlemgt0  11801  resqrexlemglsq  11803  resqrexlemga  11804  resqrtcl  11810  abslt  11870  abssubap0  11872  abssubne0  11873  caubnd2  11899  qdenre  11984  maxabslemlub  11989  maxabs  11991  maxleast  11995  fimaxre2  12009  xrmaxiflemlub  12032  xrmaxif  12035  xrmaxltsup  12042  xrmaxadd  12045  xrmineqinf  12053  climuni  12077  2clim  12085  climcn1  12092  climcn2  12093  subcn2  12095  mulcn2  12096  climsqz  12119  climsqz2  12120  climcau  12131  climcvg1nlem  12133  climcaucn  12135  serf0  12136  sumrbdclem  12162  summodclem2  12167  zsumdc  12169  divcnv  12282  absltap  12294  absgtap  12295  mertenslem2  12321  ntrivcvgap  12333  prodrbdclem  12356  prodmodclem2  12362  zproddc  12364  prodssdc  12374  fprodsplitdc  12381  fprodcl2lem  12390  efcllemp  12443  tanvalap  12493  sin01bnd  12542  cos01bnd  12543  sin01gt0  12547  absef  12555  eirrap  12563  dvds0  12591  dvdsmul1  12598  dvdsmultr1d  12617  dvdslelemd  12628  divconjdvds  12634  alzdvds  12639  3dvds  12649  sqoddm1div8z  12671  nno  12691  divalglemex  12707  bits0o  12735  dvdsbnd  12751  dvdslegcd  12759  zeqzmulgcd  12765  gcd0id  12774  gcdaddm  12779  gcd1  12782  gcdabs  12783  bezoutlemnewy  12791  bezoutlemstep  12792  bezoutlemmain  12793  bezoutlemex  12796  bezoutlemzz  12797  bezoutlemaz  12798  bezoutlembz  12799  bezoutlembi  12800  bezoutlemle  12803  bezoutlemsup  12804  mulgcd  12811  gcdzeq  12817  dvdsmulgcd  12820  sqgcd  12824  bezoutr1  12828  nninfctlemfo  12835  algcvga  12847  algfx  12848  eucalglt  12853  eucalg  12855  lcmneg  12870  lcmabs  12872  lcmgcdlem  12873  ncoprmgcdne1b  12885  mulgcddvds  12890  qredeq  12892  divgcdcoprm0  12897  cncongr1  12899  isprm2lem  12912  nprm  12919  dvdsnprmd  12921  prmdvdsfz  12936  isprm5lem  12938  coprm  12941  isprm6  12944  sqrt2irr  12959  pwbdvdslemn  12962  pwbdvdseulemle  12964  nnmaxpwlemdvds  12967  nnmaxpwlemndvds  12968  sqrt2irrap  12978  qnumdencl  12985  nn0sqdcq  13006  sqrtrirr  13007  prmdiv  13035  modprmn0modprm0  13057  prm23lt5  13064  pythagtriplem4  13069  pythagtriplem19  13083  pythagtrip  13084  pclemub  13088  pcpre1  13093  pcpremul  13094  pceulem  13095  pcqcl  13107  pcidlem  13124  pcgcd1  13129  pc2dvds  13131  dvdsprmpweqle  13138  difsqpwdvds  13139  pcadd  13141  pcmpt  13144  expnprm  13154  pockthg  13158  infpnlem2  13161  prmunb  13163  1arith  13168  4sqlem10  13188  4sqlem11  13202  4sqlem12  13203  4sqlem13m  13204  4sqlem17  13208  4sqlem18  13209  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemfrceq  13323  ennnfonelemex  13356  ennnfonelemhom  13357  ennnfonelemrnh  13358  ennnfonelemnn0  13364  ennnfonelemim  13366  exmidunben  13368  ctinfomlemom  13369  ctinfom  13370  ctinf  13372  omctfn  13385  nninfdclemp1  13392  setscomd  13444  imasaddfnlemg  13686  mhmf1o  13828  grpinveu  13894  grpasscan1  13919  dfgrp3mlem  13954  grp1inv  13963  issubg4m  14047  ghmf1o  14129  srgisid  14341  ringadd2  14383  ringinvnzdiv  14406  unitgrp  14474  ringelnzr  14545  lringuplu  14554  subrguss  14595  subrgintm  14602  aprcotr  14648  islmodd  14680  lssclg  14752  lss0cl  14757  lssvneln0  14761  lss1d  14771  lmodindp1  14816  rnglidlmmgm  14884  znidomb  15044  znunit  15045  znrrg  15046  rnasclassa  15089  mplsubgfilemcl  15142  mplsubgfileminv  15143  tgcl  15217  neii1  15300  neii2  15302  neiss  15303  tpnei  15313  tgrest  15322  ssrest  15335  icnpimaex  15364  lmcvg  15370  cnpnei  15372  cnptopco  15375  lmff  15402  txcnp  15424  txcn  15428  hmeontr  15466  blssec  15591  mopni3  15637  blsscls2  15646  comet  15652  bdxmet  15654  bdmopn  15657  xmettxlem  15662  xmettx  15663  addcncntoplem  15714  mpomulcn  15719  mulc1cncf  15742  cncfco  15744  cncfmptc  15749  mulcncflem  15760  mulcncf  15761  dedekindeulemlu  15774  dedekindeulemeu  15775  suplociccreex  15777  suplociccex  15778  dedekindicclemlu  15783  dedekindicclemeu  15784  ivthinclemlopn  15789  ivthinclemlr  15790  ivthinclemuopn  15791  ivthinclemur  15792  ivthinclemloc  15794  ivthinc  15796  ivthreinc  15798  ivthdichlem  15804  limcimolemlt  15817  limcresi  15819  cnplimcim  15820  cnplimclemle  15821  cnplimclemr  15822  limccnpcntop  15828  limccoap  15831  dvcoapbr  15860  dvcj  15862  plyf  15890  plyaddlem1  15900  plymullem1  15901  plyco  15912  plycj  15914  plycn  15915  plyrecj  15916  dvply2g  15919  efltlemlt  15927  sin0pilem2  15936  tangtx  15992  logdivlti  16036  logdivlt  16049  rplogbval  16103  logbgcd1irraplemexp  16126  logbgcd1irraplemap  16127  logbgcd1irrap  16128  zprmlogbaplem2  16138  zprmlogbap  16140  birthdaylem1g  16147  ppiublem2  16214  chtublem  16217  chtqub  16218  perfect1  16220  perfectlem1  16221  perfectlem2  16222  lgsval4a  16263  lgsdir2lem3  16271  lgsne0  16279  gausslemma2dlem3  16304  gausslemma2dlem4  16305  gausslemma2dlem6  16308  gausslemma2dlem7  16309  gausslemma2d  16310  lgseisenlem1  16311  lgsquadlem2  16319  lgsquadlem3  16320  lgsquad2lem2  16323  lgsquad3  16325  2lgsoddprmlem2  16347  2sqlem8a  16363  2sqlem8  16364  2sqlem9  16365  lpvtx  16442  upgrex  16466  upgr1een  16487  edgupgren  16504  umgredg  16508  upgrpredgv  16509  upgredg2vtx  16511  upgredgpr  16512  uspgrf1oedg  16539  usgredg4  16578  uspgredgdomord  16592  usgr1vr  16611  wlkvtxiedg  16708  wlkvtxiedgg  16709  wlk1walkdom  16722  upgriswlkdc  16723  upgrwlkedg  16724  uspgr2wlkeq  16728  uspgr2wlkeqi  16730  umgrwlknloop  16731  eupth2lem2dc  16822  trlsegvdeglem1  16823  eupth2lem3lem4fi  16836  bj-exlimmpi  16920  uzdcinzz  16948  bj-charfundcALT  16957  bj-2inf  17086  bj-peano4  17103  bj-nn0suc  17112  pw1ndom3  17142  subctctexmid  17152  exmidcon  17159  nninfalllem1  17173  nninfsellemqall  17180  nninfomnilem  17183  nninffeq  17185  nnnninfex  17187  exmidsbthrlem  17189  sbthomlem  17192  refeq  17195  isomninnlem  17201  apdifflemr  17218  redcwlpo  17227  reap0  17230  nconstwlpolem  17237