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  2851  rspcedvd  2913  sseldd  3225  ssneldd  3227  tpid3g  3782  preq12b  3848  axpweq  4255  exmid1dc  4284  exmid1stab  4292  opth  4323  issod  4410  frirrg  4441  frind  4443  ralxfr2d  4555  rexxfr2d  4556  eldifpw  4568  onun2  4582  onuni  4586  elirr  4633  en2lp  4646  wetriext  4669  peano2  4687  relop  4872  elres  5041  sotri2  5126  iota4an  5299  iota5  5300  funeu  5343  funopg  5352  imadiflem  5400  funimaexglem  5404  ssimaex  5697  ffvelcdm  5770  dff3im  5782  dffo4  5785  funopsn  5819  f1eqcocnv  5921  f1oiso2  5957  riota5f  5987  riotass2  5989  acexmidlemcase  6002  elovimad  6051  ovmpodf  6142  ovmpodv2  6144  ovi3  6148  ov6g  6149  caoftrn  6257  op1steq  6331  tfr0dm  6474  tfrlemibxssdm  6479  tfrlemi14d  6485  tfr1onlembxssdm  6495  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllembxssdm  6508  tfrcllemaccex  6513  tfrcllemres  6514  rdgivallem  6533  nnsucelsuc  6645  nnsucsssuc  6646  dcdifsnid  6658  nnawordex  6683  ersym  6700  mapvalg  6813  pmvalg  6814  mapsn  6845  fundmen  6967  en2  6981  pw2f1odclem  7003  mapdom1g  7016  fidceq  7039  fin0or  7056  findcard2  7059  findcard2s  7060  fidcen  7069  prfidceq  7101  fiintim  7104  suplub2ti  7179  supsnti  7183  supisoex  7187  difinfsnlem  7277  difinfsn  7278  ctm  7287  ctssdclemn0  7288  ctssdccl  7289  ctssdc  7291  enumctlemm  7292  nninfninc  7301  nnnninfeq2  7307  enomnilem  7316  exmidomniim  7319  exmidomni  7320  fodjuomnilemdc  7322  fodjuomnilemres  7326  omnimkv  7334  mkvprop  7336  omniwomnimkv  7345  en2prde  7377  pr2cv1  7379  en2eleq  7384  acfun  7400  exmidontriimlem1  7414  exmidontriimlem4  7417  exmidontriim  7418  ccfunen  7461  cc4f  7466  cc4n  7468  elni2  7512  mulclpi  7526  nlt1pig  7539  indpi  7540  recclnq  7590  ltexnqq  7606  halfnqq  7608  prarloclemarch  7616  prarloclemarch2  7617  prop  7673  prltlu  7685  prarloclem3step  7694  prarloclem5  7698  prarloclem  7699  prarloc  7701  prarloc2  7702  genpml  7715  genpmu  7716  genprndl  7719  genprndu  7720  genpdisj  7721  addnqprllem  7725  addnqprulem  7726  addlocprlemeq  7731  addlocprlemgt  7732  addlocprlem  7733  addlocpr  7734  nqprloc  7743  nqprl  7749  nqpru  7750  addnqprlemrl  7755  addnqprlemru  7756  appdivnq  7761  prmuloc  7764  prmuloc2  7765  mullocprlem  7768  mullocpr  7769  mulnqprlemrl  7771  mulnqprlemru  7772  ltprordil  7787  ltpopr  7793  ltsopr  7794  ltaddpr  7795  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemlol  7800  ltexprlemopu  7801  ltexprlemupu  7802  ltexprlemloc  7805  ltexprlemfl  7807  ltexprlemrl  7808  ltexprlemfu  7809  ltexprlemru  7810  ltaprg  7817  recexprlemm  7822  recexprlem1ssl  7831  recexprlem1ssu  7832  aptiprleml  7837  aptiprlemu  7838  archpr  7841  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemupu  7847  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlem1  7857  archrecpr  7862  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemupu  7870  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprlem1  7877  caucvgprlemlim  7879  caucvgprprlemnbj  7891  caucvgprprlemml  7892  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemupu  7898  caucvgprprlemdisj  7900  caucvgprprlemloc  7901  caucvgprprlemexbt  7904  caucvgprprlemaddq  7906  caucvgprprlemlim  7909  suplocexprlemss  7913  suplocexprlemrl  7915  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  suplocexprlemlub  7922  recexgt0sr  7971  mulgt0sr  7976  archsr  7980  caucvgsrlemoffcau  7996  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  cnm  8030  axarch  8089  axcaucvglemcau  8096  axpre-suploclemres  8099  lelttr  8246  ltletr  8247  ltled  8276  cnegexlem1  8332  cnegexlem2  8333  renegcl  8418  negf1o  8539  gt0add  8731  apreap  8745  apirr  8763  apsym  8764  apcotr  8765  apadd1  8766  apneg  8769  mulext1  8770  mulap0r  8773  apti  8780  aprcl  8804  aptap  8808  recexap  8811  mulap0  8812  receuap  8827  mul0eqap  8828  lep1  9003  lem1  9005  letrp1  9006  recreclt  9058  lbinf  9106  suprubex  9109  nnrecgt0  9159  bndndx  9379  nn0ge2m1nn  9440  elnn0z  9470  peano2z  9493  zaddcl  9497  ztri3or0  9499  zltnle  9503  zdceq  9533  zdcle  9534  zdclt  9535  zdiv  9546  zeo  9563  fnn0ind  9574  btwnz  9577  uzm1  9765  uzp1  9768  indstr  9800  supinfneg  9802  infsupneg  9803  eluzdc  9817  nn01to3  9824  qapne  9846  xrltled  10007  xrlelttr  10014  xrltletr  10015  ge0nemnf  10032  fzdcel  10248  elfzouz2  10370  fzoss1  10381  fzospliti  10386  elincfzoext  10411  fzocatel  10417  fzostep1  10455  zsupcllemstep  10461  zsupcl  10463  infssuzledc  10466  qtri3or  10472  qltnle  10475  qdceq  10476  qdclt  10477  exbtwnzlemex  10481  rebtwn2zlemstep  10484  rebtwn2z  10486  qbtwnxr  10489  ioom  10492  ico0  10493  ioc0  10494  flqeqceilz  10552  modqadd1  10595  modqmul1  10611  frec2uzuzd  10636  frec2uzlt2d  10638  frec2uzf1od  10640  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgdomlem  10651  uzsinds  10678  seqvalcd  10695  seqovcd  10701  seq3fveq2  10709  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  monoord  10719  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  iseqf1olemab  10736  iseqf1olemnanb  10737  iseqf1olemqk  10741  seqf1oglem1  10753  seqf1og  10755  seq3id3  10758  seq3id2  10760  seq3homo  10761  seqhomog  10764  expgt1  10811  m1expeven  10820  expnbnd  10897  expnlbnd2  10899  nn0ltexp2  10943  apexp1  10952  hashennn  11014  zfz1isolem1  11075  seq3coll  11077  pfxwrdsymbg  11237  wrdind  11269  wrd2ind  11270  cjap  11432  caucvgre  11507  cvg1nlemres  11511  resqrexlemgt0  11546  resqrexlemglsq  11548  resqrexlemga  11549  resqrtcl  11555  abslt  11614  abssubap0  11616  abssubne0  11617  caubnd2  11643  qdenre  11728  maxabslemlub  11733  maxabs  11735  maxleast  11739  fimaxre2  11753  xrmaxiflemlub  11774  xrmaxif  11777  xrmaxltsup  11784  xrmaxadd  11787  xrmineqinf  11795  climuni  11819  2clim  11827  climcn1  11834  climcn2  11835  subcn2  11837  mulcn2  11838  climsqz  11861  climsqz2  11862  climcau  11873  climcvg1nlem  11875  climcaucn  11877  serf0  11878  sumrbdclem  11903  summodclem2  11908  zsumdc  11910  divcnv  12023  absltap  12035  absgtap  12036  mertenslem2  12062  ntrivcvgap  12074  prodrbdclem  12097  prodmodclem2  12103  zproddc  12105  prodssdc  12115  fprodsplitdc  12122  fprodcl2lem  12131  efcllemp  12184  tanvalap  12234  sin01bnd  12283  cos01bnd  12284  sin01gt0  12288  absef  12296  eirrap  12304  dvds0  12332  dvdsmul1  12339  dvdsmultr1d  12358  dvdslelemd  12369  divconjdvds  12375  alzdvds  12380  3dvds  12390  sqoddm1div8z  12412  nno  12432  divalglemex  12448  bits0o  12476  dvdsbnd  12492  dvdslegcd  12500  zeqzmulgcd  12506  gcd0id  12515  gcdaddm  12520  gcd1  12523  gcdabs  12524  bezoutlemnewy  12532  bezoutlemstep  12533  bezoutlemmain  12534  bezoutlemex  12537  bezoutlemzz  12538  bezoutlemaz  12539  bezoutlembz  12540  bezoutlembi  12541  bezoutlemle  12544  bezoutlemsup  12545  mulgcd  12552  gcdzeq  12558  dvdsmulgcd  12561  sqgcd  12565  bezoutr1  12569  nninfctlemfo  12576  algcvga  12588  algfx  12589  eucalglt  12594  eucalg  12596  lcmneg  12611  lcmabs  12613  lcmgcdlem  12614  ncoprmgcdne1b  12626  mulgcddvds  12631  qredeq  12633  divgcdcoprm0  12638  cncongr1  12640  isprm2lem  12653  nprm  12660  dvdsnprmd  12662  prmdvdsfz  12676  isprm5lem  12678  coprm  12681  isprm6  12684  sqrt2irr  12699  pw2dvdslemn  12702  pw2dvdseulemle  12704  oddpwdclemdvds  12707  oddpwdclemndvds  12708  sqrt2irrap  12717  qnumdencl  12724  prmdiv  12772  modprmn0modprm0  12794  prm23lt5  12801  pythagtriplem4  12806  pythagtriplem19  12820  pythagtrip  12821  pclemub  12825  pcpre1  12830  pcpremul  12831  pceulem  12832  pcqcl  12844  pcidlem  12861  pcgcd1  12866  pc2dvds  12868  dvdsprmpweqle  12875  difsqpwdvds  12876  pcadd  12878  pcmpt  12881  expnprm  12891  pockthg  12895  infpnlem2  12898  prmunb  12900  1arith  12905  4sqlem10  12925  4sqlem11  12939  4sqlem12  12940  4sqlem13m  12941  4sqlem17  12945  4sqlem18  12946  ennnfonelemex  13000  ennnfonelemhom  13001  ennnfonelemrnh  13002  ennnfonelemnn0  13008  ennnfonelemim  13010  exmidunben  13012  ctinfomlemom  13013  ctinfom  13014  ctinf  13016  omctfn  13029  nninfdclemp1  13036  setscomd  13088  imasaddfnlemg  13362  mhmf1o  13518  grpinveu  13586  grpasscan1  13611  dfgrp3mlem  13646  grp1inv  13655  issubg4m  13745  ghmf1o  13827  srgisid  13964  ringadd2  14005  ringinvnzdiv  14028  unitgrp  14095  ringelnzr  14166  lringuplu  14175  subrguss  14215  subrgintm  14222  aprcotr  14264  islmodd  14272  lssclg  14343  lss0cl  14348  lssvneln0  14352  lss1d  14362  lmodindp1  14407  rnglidlmmgm  14475  znidomb  14637  znunit  14638  znrrg  14639  mplsubgfilemcl  14678  mplsubgfileminv  14679  tgcl  14753  neii1  14836  neii2  14838  neiss  14839  tpnei  14849  tgrest  14858  ssrest  14871  icnpimaex  14900  lmcvg  14906  cnpnei  14908  cnptopco  14911  lmff  14938  txcnp  14960  txcn  14964  hmeontr  15002  blssec  15127  mopni3  15173  blsscls2  15182  comet  15188  bdxmet  15190  bdmopn  15193  xmettxlem  15198  xmettx  15199  addcncntoplem  15250  mpomulcn  15255  mulc1cncf  15278  cncfco  15280  cncfmptc  15285  mulcncflem  15296  mulcncf  15297  dedekindeulemlu  15310  dedekindeulemeu  15311  suplociccreex  15313  suplociccex  15314  dedekindicclemlu  15319  dedekindicclemeu  15320  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemloc  15330  ivthinc  15332  ivthreinc  15334  ivthdichlem  15340  limcimolemlt  15353  limcresi  15355  cnplimcim  15356  cnplimclemle  15357  cnplimclemr  15358  limccnpcntop  15364  limccoap  15367  dvcoapbr  15396  dvcj  15398  plyf  15426  plyaddlem1  15436  plymullem1  15437  plyco  15448  plycj  15450  plycn  15451  plyrecj  15452  dvply2g  15455  efltlemlt  15463  sin0pilem2  15471  tangtx  15527  logdivlti  15570  rplogbval  15634  logbgcd1irraplemexp  15657  logbgcd1irraplemap  15658  logbgcd1irrap  15659  perfect1  15687  perfectlem1  15688  perfectlem2  15689  lgsval4a  15716  lgsdir2lem3  15724  lgsne0  15732  gausslemma2dlem3  15757  gausslemma2dlem4  15758  gausslemma2dlem6  15761  gausslemma2dlem7  15762  gausslemma2d  15763  lgseisenlem1  15764  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem2  15776  lgsquad3  15778  2lgsoddprmlem2  15800  2sqlem8a  15816  2sqlem8  15817  2sqlem9  15818  lpvtx  15894  upgrex  15918  edgupgren  15954  umgredg  15958  upgrpredgv  15959  upgredg2vtx  15961  upgredgpr  15962  uspgrf1oedg  15989  usgredg4  16028  uspgredgdomord  16042  wlkvtxiedg  16086  wlkvtxiedgg  16087  wlk1walkdom  16100  upgriswlkdc  16101  upgrwlkedg  16102  uspgr2wlkeq  16106  uspgr2wlkeqi  16108  umgrwlknloop  16109  bj-exlimmpi  16189  uzdcinzz  16217  bj-charfundcALT  16227  bj-2inf  16356  bj-peano4  16373  bj-nn0suc  16382  1dom1el  16409  pw1ndom3  16413  subctctexmid  16425  nninfalllem1  16434  nninfsellemqall  16441  nninfomnilem  16444  nninffeq  16446  nnnninfex  16448  exmidsbthrlem  16450  sbthomlem  16453  refeq  16456  isomninnlem  16458  apdifflemr  16475  redcwlpo  16483  reap0  16486  nconstwlpolem  16493