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  7341  supsnti  7345  supisoex  7349  difinfsnlem  7439  difinfsn  7440  ctm  7449  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumctlemm  7454  nninfninc  7463  nnnninfeq2  7469  enomnilem  7478  exmidomniim  7481  exmidomni  7482  fodjuomnilemdc  7484  fodjuomnilemres  7488  omnimkv  7496  mkvprop  7498  omniwomnimkv  7507  en2prde  7539  pr2cv1  7541  en2eleq  7547  acfun  7563  exmidontriimlem1  7577  exmidontriimlem4  7580  exmidontriim  7581  papsym  7612  papcotr  7613  ccfunen  7630  cc4f  7635  cc4n  7637  elni2  7681  mulclpi  7695  nlt1pig  7708  indpi  7709  recclnq  7759  ltexnqq  7775  halfnqq  7777  prarloclemarch  7785  prarloclemarch2  7786  prop  7842  prltlu  7854  prarloclem3step  7863  prarloclem5  7867  prarloclem  7868  prarloc  7870  prarloc2  7871  genpml  7884  genpmu  7885  genprndl  7888  genprndu  7889  genpdisj  7890  addnqprllem  7894  addnqprulem  7895  addlocprlemeq  7900  addlocprlemgt  7901  addlocprlem  7902  addlocpr  7903  nqprloc  7912  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  appdivnq  7930  prmuloc  7933  prmuloc2  7934  mullocprlem  7937  mullocpr  7938  mulnqprlemrl  7940  mulnqprlemru  7941  ltprordil  7956  ltpopr  7962  ltsopr  7963  ltaddpr  7964  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  ltaprg  7986  recexprlemm  7991  recexprlem1ssl  8000  recexprlem1ssu  8001  aptiprleml  8006  aptiprlemu  8007  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlem1  8026  archrecpr  8031  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlem1  8046  caucvgprlemlim  8048  caucvgprprlemnbj  8060  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemupu  8067  caucvgprprlemdisj  8069  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlemlim  8078  suplocexprlemss  8082  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  recexgt0sr  8140  mulgt0sr  8145  archsr  8149  caucvgsrlemoffcau  8165  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  cnm  8199  axarch  8258  axcaucvglemcau  8265  axpre-suploclemres  8268  lelttr  8414  ltletr  8415  ltled  8445  cnegexlem1  8501  cnegexlem2  8502  renegcl  8587  negf1o  8709  gt0add  8902  apreap  8916  apirr  8934  apsym  8935  apcotr  8936  apadd1  8937  apneg  8940  mulext1  8941  mulap0r  8944  apti  8951  aprcl  8975  aptap  8979  recexap  8982  mulap0  8983  receuap  9000  mul0eqap  9001  lep1  9176  lem1  9178  letrp1  9179  recreclt  9231  lbinf  9279  suprubex  9282  nnrecgt0  9343  bndndx  9564  nn0ge2m1nn  9629  elnn0z  9659  peano2z  9682  zaddcl  9686  ztri3or0  9688  zltnle  9692  zdceq  9722  zdcle  9723  zdclt  9724  zdiv  9736  zeo  9753  fnn0ind  9764  btwnz  9767  uzm1  9955  uzp1  9958  indstr  9995  supinfneg  9997  infsupneg  9998  eluzdc  10012  nn01to3  10019  qapne  10041  xrltled  10203  xrlelttr  10210  xrltletr  10211  ge0nemnf  10228  fzdcel  10446  elfzouz2  10571  fzoss1  10582  fzospliti  10587  elincfzoext  10613  fzocatel  10619  fzostep1  10658  zsupcllemstep  10664  zsupcl  10666  infssuzledc  10669  qtri3or  10677  qltnle  10680  qdceq  10681  qdclt  10682  exbtwnzlemex  10686  rebtwn2zlemstep  10689  rebtwn2z  10691  qbtwnxr  10694  ioom  10697  ico0  10698  ioc0  10699  flqeqceilz  10757  modqadd1  10800  modqmul1  10816  frec2uzuzd  10841  frec2uzlt2d  10843  frec2uzf1od  10845  frecuzrdgrrn  10847  frec2uzrdg  10848  frecuzrdgrcl  10849  frecuzrdgsuc  10853  frecuzrdgrclt  10854  frecuzrdgdomlem  10856  uzsinds  10883  seqvalcd  10900  seqovcd  10906  seq3fveq2  10914  seqfveq2g  10916  seq3shft2  10920  seqshft2g  10921  monoord  10924  seq3split  10927  seqsplitg  10928  seq3caopr3  10930  iseqf1olemab  10941  iseqf1olemnanb  10942  iseqf1olemqk  10946  seqf1oglem1  10958  seqf1og  10960  seq3id3  10963  seq3id2  10965  seq3homo  10966  seqhomog  10969  expgt1  11016  m1expeven  11025  expnbnd  11103  expnlbnd2  11105  nn0ltexp2  11149  apexp1  11158  hashennn  11221  hashfibclem  11284  hashf1lem2  11288  zfz1isolem1  11294  seq3coll  11296  pfxwrdsymbg  11464  wrdind  11496  wrd2ind  11497  cjap  11674  caucvgre  11749  cvg1nlemres  11753  resqrexlemgt0  11788  resqrexlemglsq  11790  resqrexlemga  11791  resqrtcl  11797  abslt  11856  abssubap0  11858  abssubne0  11859  caubnd2  11885  qdenre  11970  maxabslemlub  11975  maxabs  11977  maxleast  11981  fimaxre2  11995  xrmaxiflemlub  12016  xrmaxif  12019  xrmaxltsup  12026  xrmaxadd  12029  xrmineqinf  12037  climuni  12061  2clim  12069  climcn1  12076  climcn2  12077  subcn2  12079  mulcn2  12080  climsqz  12103  climsqz2  12104  climcau  12115  climcvg1nlem  12117  climcaucn  12119  serf0  12120  sumrbdclem  12146  summodclem2  12151  zsumdc  12153  divcnv  12266  absltap  12278  absgtap  12279  mertenslem2  12305  ntrivcvgap  12317  prodrbdclem  12340  prodmodclem2  12346  zproddc  12348  prodssdc  12358  fprodsplitdc  12365  fprodcl2lem  12374  efcllemp  12427  tanvalap  12477  sin01bnd  12526  cos01bnd  12527  sin01gt0  12531  absef  12539  eirrap  12547  dvds0  12575  dvdsmul1  12582  dvdsmultr1d  12601  dvdslelemd  12612  divconjdvds  12618  alzdvds  12623  3dvds  12633  sqoddm1div8z  12655  nno  12675  divalglemex  12691  bits0o  12719  dvdsbnd  12735  dvdslegcd  12743  zeqzmulgcd  12749  gcd0id  12758  gcdaddm  12763  gcd1  12766  gcdabs  12767  bezoutlemnewy  12775  bezoutlemstep  12776  bezoutlemmain  12777  bezoutlemex  12780  bezoutlemzz  12781  bezoutlemaz  12782  bezoutlembz  12783  bezoutlembi  12784  bezoutlemle  12787  bezoutlemsup  12788  mulgcd  12795  gcdzeq  12801  dvdsmulgcd  12804  sqgcd  12808  bezoutr1  12812  nninfctlemfo  12819  algcvga  12831  algfx  12832  eucalglt  12837  eucalg  12839  lcmneg  12854  lcmabs  12856  lcmgcdlem  12857  ncoprmgcdne1b  12869  mulgcddvds  12874  qredeq  12876  divgcdcoprm0  12881  cncongr1  12883  isprm2lem  12896  nprm  12903  dvdsnprmd  12905  prmdvdsfz  12919  isprm5lem  12921  coprm  12924  isprm6  12927  sqrt2irr  12942  pw2dvdslemn  12945  pw2dvdseulemle  12947  oddpwdclemdvds  12950  oddpwdclemndvds  12951  sqrt2irrap  12960  qnumdencl  12967  prmdiv  13015  modprmn0modprm0  13037  prm23lt5  13044  pythagtriplem4  13049  pythagtriplem19  13063  pythagtrip  13064  pclemub  13068  pcpre1  13073  pcpremul  13074  pceulem  13075  pcqcl  13087  pcidlem  13104  pcgcd1  13109  pc2dvds  13111  dvdsprmpweqle  13118  difsqpwdvds  13119  pcadd  13121  pcmpt  13124  expnprm  13134  pockthg  13138  infpnlem2  13141  prmunb  13143  1arith  13148  4sqlem10  13168  4sqlem11  13182  4sqlem12  13183  4sqlem13m  13184  4sqlem17  13188  4sqlem18  13189  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemfrceq  13274  ennnfonelemex  13307  ennnfonelemhom  13308  ennnfonelemrnh  13309  ennnfonelemnn0  13315  ennnfonelemim  13317  exmidunben  13319  ctinfomlemom  13320  ctinfom  13321  ctinf  13323  omctfn  13336  nninfdclemp1  13343  setscomd  13395  imasaddfnlemg  13637  mhmf1o  13779  grpinveu  13845  grpasscan1  13870  dfgrp3mlem  13905  grp1inv  13914  issubg4m  13998  ghmf1o  14080  srgisid  14292  ringadd2  14334  ringinvnzdiv  14357  unitgrp  14425  ringelnzr  14496  lringuplu  14505  subrguss  14546  subrgintm  14553  aprcotr  14599  islmodd  14631  lssclg  14703  lss0cl  14708  lssvneln0  14712  lss1d  14722  lmodindp1  14767  rnglidlmmgm  14835  znidomb  14995  znunit  14996  znrrg  14997  rnasclassa  15040  mplsubgfilemcl  15092  mplsubgfileminv  15093  tgcl  15167  neii1  15250  neii2  15252  neiss  15253  tpnei  15263  tgrest  15272  ssrest  15285  icnpimaex  15314  lmcvg  15320  cnpnei  15322  cnptopco  15325  lmff  15352  txcnp  15374  txcn  15378  hmeontr  15416  blssec  15541  mopni3  15587  blsscls2  15596  comet  15602  bdxmet  15604  bdmopn  15607  xmettxlem  15612  xmettx  15613  addcncntoplem  15664  mpomulcn  15669  mulc1cncf  15692  cncfco  15694  cncfmptc  15699  mulcncflem  15710  mulcncf  15711  dedekindeulemlu  15724  dedekindeulemeu  15725  suplociccreex  15727  suplociccex  15728  dedekindicclemlu  15733  dedekindicclemeu  15734  ivthinclemlopn  15739  ivthinclemlr  15740  ivthinclemuopn  15741  ivthinclemur  15742  ivthinclemloc  15744  ivthinc  15746  ivthreinc  15748  ivthdichlem  15754  limcimolemlt  15767  limcresi  15769  cnplimcim  15770  cnplimclemle  15771  cnplimclemr  15772  limccnpcntop  15778  limccoap  15781  dvcoapbr  15810  dvcj  15812  plyf  15840  plyaddlem1  15850  plymullem1  15851  plyco  15862  plycj  15864  plycn  15865  plyrecj  15866  dvply2g  15869  efltlemlt  15877  sin0pilem2  15886  tangtx  15942  logdivlti  15986  logdivlt  15999  rplogbval  16053  logbgcd1irraplemexp  16076  logbgcd1irraplemap  16077  logbgcd1irrap  16078  birthdaylem1g  16093  perfect1  16118  perfectlem1  16119  perfectlem2  16120  lgsval4a  16153  lgsdir2lem3  16161  lgsne0  16169  gausslemma2dlem3  16194  gausslemma2dlem4  16195  gausslemma2dlem6  16198  gausslemma2dlem7  16199  gausslemma2d  16200  lgseisenlem1  16201  lgsquadlem2  16209  lgsquadlem3  16210  lgsquad2lem2  16213  lgsquad3  16215  2lgsoddprmlem2  16237  2sqlem8a  16253  2sqlem8  16254  2sqlem9  16255  lpvtx  16332  upgrex  16356  upgr1een  16377  edgupgren  16394  umgredg  16398  upgrpredgv  16399  upgredg2vtx  16401  upgredgpr  16402  uspgrf1oedg  16429  usgredg4  16468  uspgredgdomord  16482  usgr1vr  16501  wlkvtxiedg  16598  wlkvtxiedgg  16599  wlk1walkdom  16612  upgriswlkdc  16613  upgrwlkedg  16614  uspgr2wlkeq  16618  uspgr2wlkeqi  16620  umgrwlknloop  16621  eupth2lem2dc  16712  trlsegvdeglem1  16713  eupth2lem3lem4fi  16726  bj-exlimmpi  16810  uzdcinzz  16838  bj-charfundcALT  16847  bj-2inf  16976  bj-peano4  16993  bj-nn0suc  17002  pw1ndom3  17032  subctctexmid  17042  exmidcon  17049  nninfalllem1  17063  nninfsellemqall  17070  nninfomnilem  17073  nninffeq  17075  nnnninfex  17077  exmidsbthrlem  17079  sbthomlem  17082  refeq  17085  isomninnlem  17091  apdifflemr  17108  redcwlpo  17117  reap0  17120  nconstwlpolem  17127