Theorem mpd 13

Description: A modus ponens deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpd.1	|- ( ph -> ps )
mpd.2	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
mpd	|- ( ph -> ch )

Proof of Theorem mpd

Step	Hyp	Ref	Expression
1		mpd.1	. 2 |- ( ph -> ps )
2		mpd.2	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	a2i 11	. 2 |- ( ( ph -> ps ) -> ( ph -> ch ) )
4	1, 3	ax-mp 5	1 |- ( ph -> ch )

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  4310  exmid1dc  4339  exmid1stab  4347  opth  4379  issod  4466  frirrg  4497  frind  4499  ralxfr2d  4612  rexxfr2d  4613  eldifpw  4625  onun2  4639  onuni  4643  elirr  4690  en2lp  4703  wetriext  4726  peano2  4744  relop  4932  elres  5101  sotri2  5188  iota4an  5361  iota5  5362  funeu  5405  funopg  5414  imadiflem  5463  funimaexglem  5467  ssimaex  5767  ffvelcdm  5844  dff3im  5856  dffo4  5859  funopsn  5894  f1eqcocnv  6000  f1oiso2  6036  riota5f  6068  riotass2  6070  acexmidlemcase  6083  elovimad  6132  ovmpodf  6223  ovmpodv2  6225  ovi3  6229  ov6g  6230  caoftrn  6339  op1steq  6417  fvdifsuppst  6488  suppssdc  6504  suppofss1dcl  6508  suppofss2dcl  6509  tfr0dm  6598  tfrlemibxssdm  6603  tfrlemi14d  6609  tfr1onlembxssdm  6619  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllembxssdm  6632  tfrcllemaccex  6637  tfrcllemres  6638  rdgivallem  6657  nnsucelsuc  6769  nnsucsssuc  6770  dcdifsnid  6782  nnawordex  6807  ersym  6824  mapvalg  6937  pmvalg  6938  mapsnd  6976  mapsn  6978  fundmen  7100  1dom1el  7113  en2  7118  pw2f1odclem  7140  mapdom1g  7153  fidceq  7177  fin0or  7196  findcard2  7199  findcard2s  7200  fidcen  7209  prfidceq  7241  fiintim  7244  funisfsuppdc  7298  suplub2ti  7347  supsnti  7351  supisoex  7355  difinfsnlem  7445  difinfsn  7446  ctm  7455  ctssdclemn0  7456  ctssdccl  7457  ctssdc  7459  enumctlemm  7460  nninfninc  7469  nnnninfeq2  7475  enomnilem  7484  exmidomniim  7487  exmidomni  7488  fodjuomnilemdc  7490  fodjuomnilemres  7494  omnimkv  7502  mkvprop  7504  omniwomnimkv  7513  en2prde  7545  pr2cv1  7547  en2eleq  7553  acfun  7569  exmidontriimlem1  7583  exmidontriimlem4  7586  exmidontriim  7587  papsym  7618  papcotr  7619  ccfunen  7636  cc4f  7641  cc4n  7643  elni2  7687  mulclpi  7701  nlt1pig  7714  indpi  7715  recclnq  7765  ltexnqq  7781  halfnqq  7783  prarloclemarch  7791  prarloclemarch2  7792  prop  7848  prltlu  7860  prarloclem3step  7869  prarloclem5  7873  prarloclem  7874  prarloc  7876  prarloc2  7877  genpml  7890  genpmu  7891  genprndl  7894  genprndu  7895  genpdisj  7896  addnqprllem  7900  addnqprulem  7901  addlocprlemeq  7906  addlocprlemgt  7907  addlocprlem  7908  addlocpr  7909  nqprloc  7918  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  appdivnq  7936  prmuloc  7939  prmuloc2  7940  mullocprlem  7943  mullocpr  7944  mulnqprlemrl  7946  mulnqprlemru  7947  ltprordil  7962  ltpopr  7968  ltsopr  7969  ltaddpr  7970  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  ltexprlemloc  7980  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  ltaprg  7992  recexprlemm  7997  recexprlem1ssl  8006  recexprlem1ssu  8007  aptiprleml  8012  aptiprlemu  8013  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlem1  8032  archrecpr  8037  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlem1  8052  caucvgprlemlim  8054  caucvgprprlemnbj  8066  caucvgprprlemml  8067  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemopu  8072  caucvgprprlemupu  8073  caucvgprprlemdisj  8075  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  caucvgprprlemaddq  8081  caucvgprprlemlim  8084  suplocexprlemss  8088  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  suplocexprlemlub  8097  recexgt0sr  8146  mulgt0sr  8151  archsr  8155  caucvgsrlemoffcau  8171  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  cnm  8205  axarch  8264  axcaucvglemcau  8271  axpre-suploclemres  8274  lelttr  8420  ltletr  8421  ltled  8452  cnegexlem1  8508  cnegexlem2  8509  renegcl  8594  negf1o  8716  gt0add  8909  apreap  8923  apirr  8941  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  mulap0r  8951  apti  8958  aprcl  8982  aptap  8986  recexap  8989  mulap0  8990  receuap  9007  mul0eqap  9008  lep1  9183  lem1  9185  letrp1  9186  recreclt  9238  lbinf  9286  suprubex  9289  nnrecgt0  9351  bndndx  9573  nn0ge2m1nn  9636  elnn0z  9666  peano2z  9689  zaddcl  9693  ztri3or0  9695  zltnle  9699  zdceq  9729  zdcle  9730  zdclt  9731  zdiv  9744  zeo  9761  fnn0ind  9772  btwnz  9775  uzm1  9968  uzp1  9971  indstr  10008  supinfneg  10010  infsupneg  10011  eluzdc  10025  nn01to3  10032  qapne  10054  xrltled  10217  xrlelttr  10224  xrltletr  10225  ge0nemnf  10242  fzdcel  10460  elfzouz2  10585  fzoss1  10596  fzospliti  10601  elincfzoext  10627  fzocatel  10633  fzostep1  10672  zsupcllemstep  10678  zsupcl  10680  infssuzledc  10683  qtri3or  10691  qltnle  10694  qdceq  10695  qdclt  10696  exbtwnzlemex  10700  rebtwn2zlemstep  10703  rebtwn2z  10705  qbtwnxr  10708  ioom  10711  ico0  10712  ioc0  10713  flqeqceilz  10775  modqadd1  10818  modqmul1  10834  frec2uzuzd  10859  frec2uzlt2d  10861  frec2uzf1od  10863  frecuzrdgrrn  10865  frec2uzrdg  10866  frecuzrdgrcl  10867  frecuzrdgsuc  10871  frecuzrdgrclt  10872  frecuzrdgdomlem  10874  uzsinds  10901  seqvalcd  10918  seqovcd  10924  seq3fveq2  10932  seqfveq2g  10934  seq3shft2  10938  seqshft2g  10939  monoord  10942  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  iseqf1olemab  10959  iseqf1olemnanb  10960  iseqf1olemqk  10964  seqf1oglem1  10976  seqf1og  10978  seq3id3  10981  seq3id2  10983  seq3homo  10984  seqhomog  10987  expgt1  11034  m1expeven  11043  expnbnd  11121  expnlbnd2  11123  nn0ltexp2  11168  apexp1  11177  hashennn  11240  hashfibclem  11303  hashf1lem2  11307  zfz1isolem1  11313  seq3coll  11315  pfxwrdsymbg  11483  wrdind  11515  wrd2ind  11516  cjap  11693  caucvgre  11768  cvg1nlemres  11772  resqrexlemgt0  11807  resqrexlemglsq  11809  resqrexlemga  11810  resqrtcl  11816  abslt  11876  abssubap0  11878  abssubne0  11879  caubnd2  11905  qdenre  11990  maxabslemlub  11995  maxabs  11997  maxleast  12001  fimaxre2  12015  xrmaxiflemlub  12038  xrmaxif  12041  xrmaxltsup  12048  xrmaxadd  12051  xrmineqinf  12059  climuni  12083  2clim  12091  climcn1  12098  climcn2  12099  subcn2  12101  mulcn2  12102  climsqz  12125  climsqz2  12126  climcau  12137  climcvg1nlem  12139  climcaucn  12141  serf0  12142  sumrbdclem  12168  summodclem2  12173  zsumdc  12175  divcnv  12288  absltap  12300  absgtap  12301  mertenslem2  12327  ntrivcvgap  12339  prodrbdclem  12362  prodmodclem2  12368  zproddc  12370  prodssdc  12380  fprodsplitdc  12387  fprodcl2lem  12396  efcllemp  12449  tanvalap  12499  sin01bnd  12548  cos01bnd  12549  sin01gt0  12553  absef  12561  eirrap  12569  dvds0  12597  dvdsmul1  12604  dvdsmultr1d  12623  dvdslelemd  12634  divconjdvds  12640  alzdvds  12645  3dvds  12655  sqoddm1div8z  12677  nno  12697  divalglemex  12713  bits0o  12741  dvdsbnd  12757  dvdslegcd  12765  zeqzmulgcd  12771  gcd0id  12780  gcdaddm  12785  gcd1  12788  gcdabs  12789  bezoutlemnewy  12797  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlemex  12802  bezoutlemzz  12803  bezoutlemaz  12804  bezoutlembz  12805  bezoutlembi  12806  bezoutlemle  12809  bezoutlemsup  12810  mulgcd  12817  gcdzeq  12823  dvdsmulgcd  12826  sqgcd  12830  bezoutr1  12834  nninfctlemfo  12841  algcvga  12853  algfx  12854  eucalglt  12859  eucalg  12861  lcmneg  12876  lcmabs  12878  lcmgcdlem  12879  ncoprmgcdne1b  12891  mulgcddvds  12896  qredeq  12898  divgcdcoprm0  12903  cncongr1  12905  isprm2lem  12918  nprm  12925  dvdsnprmd  12927  prmdvdsfz  12942  isprm5lem  12944  coprm  12947  isprm6  12950  sqrt2irr  12965  pwbdvdslemn  12968  pwbdvdseulemle  12970  nnmaxpwlemdvds  12973  nnmaxpwlemndvds  12974  sqrt2irrap  12984  qnumdencl  12991  nn0sqdcq  13012  sqrtrirr  13013  prmdiv  13041  modprmn0modprm0  13063  prm23lt5  13070  pythagtriplem4  13075  pythagtriplem19  13089  pythagtrip  13090  pclemub  13094  pcpre1  13099  pcpremul  13100  pceulem  13101  pcqcl  13113  pcidlem  13130  pcgcd1  13135  pc2dvds  13137  dvdsprmpweqle  13144  difsqpwdvds  13145  pcadd  13147  pcmpt  13150  expnprm  13160  pockthg  13164  infpnlem2  13167  prmunb  13169  1arith  13174  4sqlem10  13194  4sqlem11  13208  4sqlem12  13209  4sqlem13m  13210  4sqlem17  13214  4sqlem18  13215  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfrceq  13329  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemrnh  13364  ennnfonelemnn0  13370  ennnfonelemim  13372  exmidunben  13374  ctinfomlemom  13375  ctinfom  13376  ctinf  13378  omctfn  13391  nninfdclemp1  13398  setscomd  13450  imasaddfnlemg  13693  mhmf1o  13835  grpinveu  13901  grpasscan1  13926  dfgrp3mlem  13961  grp1inv  13970  issubg4m  14054  ghmf1o  14136  gsum2d2fi  14273  srgisid  14396  ringadd2  14438  ringinvnzdiv  14461  unitgrp  14531  ringelnzr  14602  lringuplu  14611  subrguss  14652  subrgintm  14659  aprcotr  14705  islmodd  14737  lssclg  14809  lss0cl  14814  lssvneln0  14818  lss1d  14828  lmodindp1  14873  rnglidlmmgm  14941  znidomb  15101  znunit  15102  znrrg  15103  rnasclassa  15146  mvrf1fi  15219  mplsubgfileminv  15233  tgcl  15307  neii1  15390  neii2  15392  neiss  15393  tpnei  15403  tgrest  15412  ssrest  15425  icnpimaex  15454  lmcvg  15460  cnpnei  15462  cnptopco  15465  lmff  15492  txcnp  15514  txcn  15518  hmeontr  15556  blssec  15681  mopni3  15727  blsscls2  15736  comet  15742  bdxmet  15744  bdmopn  15747  xmettxlem  15752  xmettx  15753  addcncntoplem  15804  mpomulcn  15809  mulc1cncf  15832  cncfco  15834  cncfmptc  15839  mulcncflem  15850  mulcncf  15851  dedekindeulemlu  15864  dedekindeulemeu  15865  suplociccreex  15867  suplociccex  15868  dedekindicclemlu  15873  dedekindicclemeu  15874  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemloc  15884  ivthinc  15886  ivthreinc  15888  ivthdichlem  15894  limcimolemlt  15907  limcresi  15909  cnplimcim  15910  cnplimclemle  15911  cnplimclemr  15912  limccnpcntop  15918  limccoap  15921  dvcoapbr  15950  dvcj  15952  plyf  15980  plyaddlem1  15990  plymullem1  15991  plyco  16002  plycj  16004  plycn  16005  plyrecj  16006  dvply2g  16009  efltlemlt  16017  sin0pilem2  16026  tangtx  16082  logdivlti  16128  logdivlt  16141  rplogbval  16198  logbgcd1irraplemexp  16221  logbgcd1irraplemap  16222  logbgcd1irrap  16223  zprmlogbaplem2  16233  zprmlogbap  16235  birthdaylem1g  16242  ppiublem2  16309  chtublem  16312  chtqub  16313  perfect1  16315  perfectlem1  16316  perfectlem2  16317  bposlem6  16333  bposlem9  16336  bpos  16337  lgsval4a  16363  lgsdir2lem3  16371  lgsne0  16379  gausslemma2dlem3  16404  gausslemma2dlem4  16405  gausslemma2dlem6  16408  gausslemma2dlem7  16409  gausslemma2d  16410  lgseisenlem1  16411  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2lem2  16423  lgsquad3  16425  2lgsoddprmlem2  16447  2sqlem8a  16463  2sqlem8  16464  2sqlem9  16465  lpvtx  16542  upgrex  16566  upgr1een  16587  edgupgren  16604  umgredg  16608  upgrpredgv  16609  upgredg2vtx  16611  upgredgpr  16612  uspgrf1oedg  16639  usgredg4  16678  uspgredgdomord  16692  usgr1vr  16711  wlkvtxiedg  16808  wlkvtxiedgg  16809  wlk1walkdom  16822  upgriswlkdc  16823  upgrwlkedg  16824  uspgr2wlkeq  16828  uspgr2wlkeqi  16830  umgrwlknloop  16831  eupth2lem2dc  16922  trlsegvdeglem1  16923  eupth2lem3lem4fi  16936  bj-exlimmpi  17020  uzdcinzz  17048  bj-charfundcALT  17057  bj-2inf  17186  bj-peano4  17203  bj-nn0suc  17212  pw1ndom3  17242  subctctexmid  17252  exmidcon  17259  nninfalllem1  17274  nninfsellemqall  17281  nninfomnilem  17284  nninffeq  17286  nnnninfex  17288  exmidsbthrlem  17290  sbthomlem  17293  refeq  17296  isomninnlem  17302  apdifflemr  17320  redcwlpo  17329  reap0  17332  nconstwlpolem  17339