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 )

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  2852  rspcedvd  2914  sseldd  3226  ssneldd  3228  tpid3g  3785  preq12b  3851  axpweq  4259  exmid1dc  4288  exmid1stab  4296  opth  4327  issod  4414  frirrg  4445  frind  4447  ralxfr2d  4559  rexxfr2d  4560  eldifpw  4572  onun2  4586  onuni  4590  elirr  4637  en2lp  4650  wetriext  4673  peano2  4691  relop  4878  elres  5047  sotri2  5132  iota4an  5305  iota5  5306  funeu  5349  funopg  5358  imadiflem  5406  funimaexglem  5410  ssimaex  5703  ffvelcdm  5776  dff3im  5788  dffo4  5791  funopsn  5825  f1eqcocnv  5927  f1oiso2  5963  riota5f  5993  riotass2  5995  acexmidlemcase  6008  elovimad  6057  ovmpodf  6148  ovmpodv2  6150  ovi3  6154  ov6g  6155  caoftrn  6263  op1steq  6337  tfr0dm  6483  tfrlemibxssdm  6488  tfrlemi14d  6494  tfr1onlembxssdm  6504  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllembxssdm  6517  tfrcllemaccex  6522  tfrcllemres  6523  rdgivallem  6542  nnsucelsuc  6654  nnsucsssuc  6655  dcdifsnid  6667  nnawordex  6692  ersym  6709  mapvalg  6822  pmvalg  6823  mapsn  6854  fundmen  6976  1dom1el  6988  en2  6993  pw2f1odclem  7015  mapdom1g  7028  fidceq  7051  fin0or  7068  findcard2  7071  findcard2s  7072  fidcen  7081  prfidceq  7113  fiintim  7116  suplub2ti  7191  supsnti  7195  supisoex  7199  difinfsnlem  7289  difinfsn  7290  ctm  7299  ctssdclemn0  7300  ctssdccl  7301  ctssdc  7303  enumctlemm  7304  nninfninc  7313  nnnninfeq2  7319  enomnilem  7328  exmidomniim  7331  exmidomni  7332  fodjuomnilemdc  7334  fodjuomnilemres  7338  omnimkv  7346  mkvprop  7348  omniwomnimkv  7357  en2prde  7389  pr2cv1  7391  en2eleq  7396  acfun  7412  exmidontriimlem1  7426  exmidontriimlem4  7429  exmidontriim  7430  ccfunen  7473  cc4f  7478  cc4n  7480  elni2  7524  mulclpi  7538  nlt1pig  7551  indpi  7552  recclnq  7602  ltexnqq  7618  halfnqq  7620  prarloclemarch  7628  prarloclemarch2  7629  prop  7685  prltlu  7697  prarloclem3step  7706  prarloclem5  7710  prarloclem  7711  prarloc  7713  prarloc2  7714  genpml  7727  genpmu  7728  genprndl  7731  genprndu  7732  genpdisj  7733  addnqprllem  7737  addnqprulem  7738  addlocprlemeq  7743  addlocprlemgt  7744  addlocprlem  7745  addlocpr  7746  nqprloc  7755  nqprl  7761  nqpru  7762  addnqprlemrl  7767  addnqprlemru  7768  appdivnq  7773  prmuloc  7776  prmuloc2  7777  mullocprlem  7780  mullocpr  7781  mulnqprlemrl  7783  mulnqprlemru  7784  ltprordil  7799  ltpopr  7805  ltsopr  7806  ltaddpr  7807  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  ltexprlemloc  7817  ltexprlemfl  7819  ltexprlemrl  7820  ltexprlemfu  7821  ltexprlemru  7822  ltaprg  7829  recexprlemm  7834  recexprlem1ssl  7843  recexprlem1ssu  7844  aptiprleml  7849  aptiprlemu  7850  archpr  7853  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemopu  7858  cauappcvgprlemupu  7859  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  cauappcvgprlem1  7869  archrecpr  7874  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemopu  7881  caucvgprlemupu  7882  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemladdfu  7887  caucvgprlem1  7889  caucvgprlemlim  7891  caucvgprprlemnbj  7903  caucvgprprlemml  7904  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemupu  7910  caucvgprprlemdisj  7912  caucvgprprlemloc  7913  caucvgprprlemexbt  7916  caucvgprprlemaddq  7918  caucvgprprlemlim  7921  suplocexprlemss  7925  suplocexprlemrl  7927  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  suplocexprlemlub  7934  recexgt0sr  7983  mulgt0sr  7988  archsr  7992  caucvgsrlemoffcau  8008  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  cnm  8042  axarch  8101  axcaucvglemcau  8108  axpre-suploclemres  8111  lelttr  8258  ltletr  8259  ltled  8288  cnegexlem1  8344  cnegexlem2  8345  renegcl  8430  negf1o  8551  gt0add  8743  apreap  8757  apirr  8775  apsym  8776  apcotr  8777  apadd1  8778  apneg  8781  mulext1  8782  mulap0r  8785  apti  8792  aprcl  8816  aptap  8820  recexap  8823  mulap0  8824  receuap  8839  mul0eqap  8840  lep1  9015  lem1  9017  letrp1  9018  recreclt  9070  lbinf  9118  suprubex  9121  nnrecgt0  9171  bndndx  9391  nn0ge2m1nn  9452  elnn0z  9482  peano2z  9505  zaddcl  9509  ztri3or0  9511  zltnle  9515  zdceq  9545  zdcle  9546  zdclt  9547  zdiv  9558  zeo  9575  fnn0ind  9586  btwnz  9589  uzm1  9777  uzp1  9780  indstr  9817  supinfneg  9819  infsupneg  9820  eluzdc  9834  nn01to3  9841  qapne  9863  xrltled  10024  xrlelttr  10031  xrltletr  10032  ge0nemnf  10049  fzdcel  10265  elfzouz2  10387  fzoss1  10398  fzospliti  10403  elincfzoext  10428  fzocatel  10434  fzostep1  10473  zsupcllemstep  10479  zsupcl  10481  infssuzledc  10484  qtri3or  10490  qltnle  10493  qdceq  10494  qdclt  10495  exbtwnzlemex  10499  rebtwn2zlemstep  10502  rebtwn2z  10504  qbtwnxr  10507  ioom  10510  ico0  10511  ioc0  10512  flqeqceilz  10570  modqadd1  10613  modqmul1  10629  frec2uzuzd  10654  frec2uzlt2d  10656  frec2uzf1od  10658  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgsuc  10666  frecuzrdgrclt  10667  frecuzrdgdomlem  10669  uzsinds  10696  seqvalcd  10713  seqovcd  10719  seq3fveq2  10727  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  monoord  10737  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  iseqf1olemab  10754  iseqf1olemnanb  10755  iseqf1olemqk  10759  seqf1oglem1  10771  seqf1og  10773  seq3id3  10776  seq3id2  10778  seq3homo  10779  seqhomog  10782  expgt1  10829  m1expeven  10838  expnbnd  10915  expnlbnd2  10917  nn0ltexp2  10961  apexp1  10970  hashennn  11032  zfz1isolem1  11094  seq3coll  11096  pfxwrdsymbg  11261  wrdind  11293  wrd2ind  11294  cjap  11457  caucvgre  11532  cvg1nlemres  11536  resqrexlemgt0  11571  resqrexlemglsq  11573  resqrexlemga  11574  resqrtcl  11580  abslt  11639  abssubap0  11641  abssubne0  11642  caubnd2  11668  qdenre  11753  maxabslemlub  11758  maxabs  11760  maxleast  11764  fimaxre2  11778  xrmaxiflemlub  11799  xrmaxif  11802  xrmaxltsup  11809  xrmaxadd  11812  xrmineqinf  11820  climuni  11844  2clim  11852  climcn1  11859  climcn2  11860  subcn2  11862  mulcn2  11863  climsqz  11886  climsqz2  11887  climcau  11898  climcvg1nlem  11900  climcaucn  11902  serf0  11903  sumrbdclem  11928  summodclem2  11933  zsumdc  11935  divcnv  12048  absltap  12060  absgtap  12061  mertenslem2  12087  ntrivcvgap  12099  prodrbdclem  12122  prodmodclem2  12128  zproddc  12130  prodssdc  12140  fprodsplitdc  12147  fprodcl2lem  12156  efcllemp  12209  tanvalap  12259  sin01bnd  12308  cos01bnd  12309  sin01gt0  12313  absef  12321  eirrap  12329  dvds0  12357  dvdsmul1  12364  dvdsmultr1d  12383  dvdslelemd  12394  divconjdvds  12400  alzdvds  12405  3dvds  12415  sqoddm1div8z  12437  nno  12457  divalglemex  12473  bits0o  12501  dvdsbnd  12517  dvdslegcd  12525  zeqzmulgcd  12531  gcd0id  12540  gcdaddm  12545  gcd1  12548  gcdabs  12549  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlemex  12562  bezoutlemzz  12563  bezoutlemaz  12564  bezoutlembz  12565  bezoutlembi  12566  bezoutlemle  12569  bezoutlemsup  12570  mulgcd  12577  gcdzeq  12583  dvdsmulgcd  12586  sqgcd  12590  bezoutr1  12594  nninfctlemfo  12601  algcvga  12613  algfx  12614  eucalglt  12619  eucalg  12621  lcmneg  12636  lcmabs  12638  lcmgcdlem  12639  ncoprmgcdne1b  12651  mulgcddvds  12656  qredeq  12658  divgcdcoprm0  12663  cncongr1  12665  isprm2lem  12678  nprm  12685  dvdsnprmd  12687  prmdvdsfz  12701  isprm5lem  12703  coprm  12706  isprm6  12709  sqrt2irr  12724  pw2dvdslemn  12727  pw2dvdseulemle  12729  oddpwdclemdvds  12732  oddpwdclemndvds  12733  sqrt2irrap  12742  qnumdencl  12749  prmdiv  12797  modprmn0modprm0  12819  prm23lt5  12826  pythagtriplem4  12831  pythagtriplem19  12845  pythagtrip  12846  pclemub  12850  pcpre1  12855  pcpremul  12856  pceulem  12857  pcqcl  12869  pcidlem  12886  pcgcd1  12891  pc2dvds  12893  dvdsprmpweqle  12900  difsqpwdvds  12901  pcadd  12903  pcmpt  12906  expnprm  12916  pockthg  12920  infpnlem2  12923  prmunb  12925  1arith  12930  4sqlem10  12950  4sqlem11  12964  4sqlem12  12965  4sqlem13m  12966  4sqlem17  12970  4sqlem18  12971  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemrnh  13027  ennnfonelemnn0  13033  ennnfonelemim  13035  exmidunben  13037  ctinfomlemom  13038  ctinfom  13039  ctinf  13041  omctfn  13054  nninfdclemp1  13061  setscomd  13113  imasaddfnlemg  13387  mhmf1o  13543  grpinveu  13611  grpasscan1  13636  dfgrp3mlem  13671  grp1inv  13680  issubg4m  13770  ghmf1o  13852  srgisid  13989  ringadd2  14030  ringinvnzdiv  14053  unitgrp  14120  ringelnzr  14191  lringuplu  14200  subrguss  14240  subrgintm  14247  aprcotr  14289  islmodd  14297  lssclg  14368  lss0cl  14373  lssvneln0  14377  lss1d  14387  lmodindp1  14432  rnglidlmmgm  14500  znidomb  14662  znunit  14663  znrrg  14664  mplsubgfilemcl  14703  mplsubgfileminv  14704  tgcl  14778  neii1  14861  neii2  14863  neiss  14864  tpnei  14874  tgrest  14883  ssrest  14896  icnpimaex  14925  lmcvg  14931  cnpnei  14933  cnptopco  14936  lmff  14963  txcnp  14985  txcn  14989  hmeontr  15027  blssec  15152  mopni3  15198  blsscls2  15207  comet  15213  bdxmet  15215  bdmopn  15218  xmettxlem  15223  xmettx  15224  addcncntoplem  15275  mpomulcn  15280  mulc1cncf  15303  cncfco  15305  cncfmptc  15310  mulcncflem  15321  mulcncf  15322  dedekindeulemlu  15335  dedekindeulemeu  15336  suplociccreex  15338  suplociccex  15339  dedekindicclemlu  15344  dedekindicclemeu  15345  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemloc  15355  ivthinc  15357  ivthreinc  15359  ivthdichlem  15365  limcimolemlt  15378  limcresi  15380  cnplimcim  15381  cnplimclemle  15382  cnplimclemr  15383  limccnpcntop  15389  limccoap  15392  dvcoapbr  15421  dvcj  15423  plyf  15451  plyaddlem1  15461  plymullem1  15462  plyco  15473  plycj  15475  plycn  15476  plyrecj  15477  dvply2g  15480  efltlemlt  15488  sin0pilem2  15496  tangtx  15552  logdivlti  15595  rplogbval  15659  logbgcd1irraplemexp  15682  logbgcd1irraplemap  15683  logbgcd1irrap  15684  perfect1  15712  perfectlem1  15713  perfectlem2  15714  lgsval4a  15741  lgsdir2lem3  15749  lgsne0  15757  gausslemma2dlem3  15782  gausslemma2dlem4  15783  gausslemma2dlem6  15786  gausslemma2dlem7  15787  gausslemma2d  15788  lgseisenlem1  15789  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem2  15801  lgsquad3  15803  2lgsoddprmlem2  15825  2sqlem8a  15841  2sqlem8  15842  2sqlem9  15843  lpvtx  15920  upgrex  15944  edgupgren  15980  umgredg  15984  upgrpredgv  15985  upgredg2vtx  15987  upgredgpr  15988  uspgrf1oedg  16015  usgredg4  16054  uspgredgdomord  16068  usgr1vr  16087  wlkvtxiedg  16142  wlkvtxiedgg  16143  wlk1walkdom  16156  upgriswlkdc  16157  upgrwlkedg  16158  uspgr2wlkeq  16162  uspgr2wlkeqi  16164  umgrwlknloop  16165  bj-exlimmpi  16302  uzdcinzz  16330  bj-charfundcALT  16340  bj-2inf  16469  bj-peano4  16486  bj-nn0suc  16495  pw1ndom3  16525  subctctexmid  16537  nninfalllem1  16546  nninfsellemqall  16553  nninfomnilem  16556  nninffeq  16558  nnnninfex  16560  exmidsbthrlem  16562  sbthomlem  16565  refeq  16568  isomninnlem  16570  apdifflemr  16587  redcwlpo  16595  reap0  16598  nconstwlpolem  16605