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  625  mt2d  630  mpnanrd  699  mpjaod  725  stdcndcOLD  853  impidc  865  jadc  870  pm2.54dc  898  oplem1  983  mp3and  1376  xor3dc  1431  exlimdd  1920  exlimddv  1947  eqrdav  2230  necon1aidc  2453  necon1bidc  2454  necon4aidc  2470  reximddv  2635  reximssdv  2636  rexlimddv  2655  vtoclgft  2854  rspcedvd  2916  sseldd  3228  ssneldd  3230  tpid3g  3787  preq12b  3853  axpweq  4261  exmid1dc  4290  exmid1stab  4298  opth  4329  issod  4416  frirrg  4447  frind  4449  ralxfr2d  4561  rexxfr2d  4562  eldifpw  4574  onun2  4588  onuni  4592  elirr  4639  en2lp  4652  wetriext  4675  peano2  4693  relop  4880  elres  5049  sotri2  5134  iota4an  5307  iota5  5308  funeu  5351  funopg  5360  imadiflem  5409  funimaexglem  5413  ssimaex  5707  ffvelcdm  5780  dff3im  5792  dffo4  5795  funopsn  5830  f1eqcocnv  5932  f1oiso2  5968  riota5f  5998  riotass2  6000  acexmidlemcase  6013  elovimad  6062  ovmpodf  6153  ovmpodv2  6155  ovi3  6159  ov6g  6160  caoftrn  6268  op1steq  6342  tfr0dm  6488  tfrlemibxssdm  6493  tfrlemi14d  6499  tfr1onlembxssdm  6509  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllembxssdm  6522  tfrcllemaccex  6527  tfrcllemres  6528  rdgivallem  6547  nnsucelsuc  6659  nnsucsssuc  6660  dcdifsnid  6672  nnawordex  6697  ersym  6714  mapvalg  6827  pmvalg  6828  mapsn  6859  fundmen  6981  1dom1el  6993  en2  6998  pw2f1odclem  7020  mapdom1g  7033  fidceq  7056  fin0or  7075  findcard2  7078  findcard2s  7079  fidcen  7088  prfidceq  7120  fiintim  7123  suplub2ti  7200  supsnti  7204  supisoex  7208  difinfsnlem  7298  difinfsn  7299  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  nninfninc  7322  nnnninfeq2  7328  enomnilem  7337  exmidomniim  7340  exmidomni  7341  fodjuomnilemdc  7343  fodjuomnilemres  7347  omnimkv  7355  mkvprop  7357  omniwomnimkv  7366  en2prde  7398  pr2cv1  7400  en2eleq  7406  acfun  7422  exmidontriimlem1  7436  exmidontriimlem4  7439  exmidontriim  7440  ccfunen  7483  cc4f  7488  cc4n  7490  elni2  7534  mulclpi  7548  nlt1pig  7561  indpi  7562  recclnq  7612  ltexnqq  7628  halfnqq  7630  prarloclemarch  7638  prarloclemarch2  7639  prop  7695  prltlu  7707  prarloclem3step  7716  prarloclem5  7720  prarloclem  7721  prarloc  7723  prarloc2  7724  genpml  7737  genpmu  7738  genprndl  7741  genprndu  7742  genpdisj  7743  addnqprllem  7747  addnqprulem  7748  addlocprlemeq  7753  addlocprlemgt  7754  addlocprlem  7755  addlocpr  7756  nqprloc  7765  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  appdivnq  7783  prmuloc  7786  prmuloc2  7787  mullocprlem  7790  mullocpr  7791  mulnqprlemrl  7793  mulnqprlemru  7794  ltprordil  7809  ltpopr  7815  ltsopr  7816  ltaddpr  7817  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemloc  7827  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  ltaprg  7839  recexprlemm  7844  recexprlem1ssl  7853  recexprlem1ssu  7854  aptiprleml  7859  aptiprlemu  7860  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlem1  7879  archrecpr  7884  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlem1  7899  caucvgprlemlim  7901  caucvgprprlemnbj  7913  caucvgprprlemml  7914  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemupu  7920  caucvgprprlemdisj  7922  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlemaddq  7928  caucvgprprlemlim  7931  suplocexprlemss  7935  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  recexgt0sr  7993  mulgt0sr  7998  archsr  8002  caucvgsrlemoffcau  8018  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  cnm  8052  axarch  8111  axcaucvglemcau  8118  axpre-suploclemres  8121  lelttr  8268  ltletr  8269  ltled  8298  cnegexlem1  8354  cnegexlem2  8355  renegcl  8440  negf1o  8561  gt0add  8753  apreap  8767  apirr  8785  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  mulap0r  8795  apti  8802  aprcl  8826  aptap  8830  recexap  8833  mulap0  8834  receuap  8849  mul0eqap  8850  lep1  9025  lem1  9027  letrp1  9028  recreclt  9080  lbinf  9128  suprubex  9131  nnrecgt0  9181  bndndx  9401  nn0ge2m1nn  9462  elnn0z  9492  peano2z  9515  zaddcl  9519  ztri3or0  9521  zltnle  9525  zdceq  9555  zdcle  9556  zdclt  9557  zdiv  9568  zeo  9585  fnn0ind  9596  btwnz  9599  uzm1  9787  uzp1  9790  indstr  9827  supinfneg  9829  infsupneg  9830  eluzdc  9844  nn01to3  9851  qapne  9873  xrltled  10034  xrlelttr  10041  xrltletr  10042  ge0nemnf  10059  fzdcel  10275  elfzouz2  10397  fzoss1  10408  fzospliti  10413  elincfzoext  10439  fzocatel  10445  fzostep1  10484  zsupcllemstep  10490  zsupcl  10492  infssuzledc  10495  qtri3or  10501  qltnle  10504  qdceq  10505  qdclt  10506  exbtwnzlemex  10510  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnxr  10518  ioom  10521  ico0  10522  ioc0  10523  flqeqceilz  10581  modqadd1  10624  modqmul1  10640  frec2uzuzd  10665  frec2uzlt2d  10667  frec2uzf1od  10669  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgdomlem  10680  uzsinds  10707  seqvalcd  10724  seqovcd  10730  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  iseqf1olemab  10765  iseqf1olemnanb  10766  iseqf1olemqk  10770  seqf1oglem1  10782  seqf1og  10784  seq3id3  10787  seq3id2  10789  seq3homo  10790  seqhomog  10793  expgt1  10840  m1expeven  10849  expnbnd  10926  expnlbnd2  10928  nn0ltexp2  10972  apexp1  10981  hashennn  11043  zfz1isolem1  11105  seq3coll  11107  pfxwrdsymbg  11275  wrdind  11307  wrd2ind  11308  cjap  11484  caucvgre  11559  cvg1nlemres  11563  resqrexlemgt0  11598  resqrexlemglsq  11600  resqrexlemga  11601  resqrtcl  11607  abslt  11666  abssubap0  11668  abssubne0  11669  caubnd2  11695  qdenre  11780  maxabslemlub  11785  maxabs  11787  maxleast  11791  fimaxre2  11805  xrmaxiflemlub  11826  xrmaxif  11829  xrmaxltsup  11836  xrmaxadd  11839  xrmineqinf  11847  climuni  11871  2clim  11879  climcn1  11886  climcn2  11887  subcn2  11889  mulcn2  11890  climsqz  11913  climsqz2  11914  climcau  11925  climcvg1nlem  11927  climcaucn  11929  serf0  11930  sumrbdclem  11956  summodclem2  11961  zsumdc  11963  divcnv  12076  absltap  12088  absgtap  12089  mertenslem2  12115  ntrivcvgap  12127  prodrbdclem  12150  prodmodclem2  12156  zproddc  12158  prodssdc  12168  fprodsplitdc  12175  fprodcl2lem  12184  efcllemp  12237  tanvalap  12287  sin01bnd  12336  cos01bnd  12337  sin01gt0  12341  absef  12349  eirrap  12357  dvds0  12385  dvdsmul1  12392  dvdsmultr1d  12411  dvdslelemd  12422  divconjdvds  12428  alzdvds  12433  3dvds  12443  sqoddm1div8z  12465  nno  12485  divalglemex  12501  bits0o  12529  dvdsbnd  12545  dvdslegcd  12553  zeqzmulgcd  12559  gcd0id  12568  gcdaddm  12573  gcd1  12576  gcdabs  12577  bezoutlemnewy  12585  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlemex  12590  bezoutlemzz  12591  bezoutlemaz  12592  bezoutlembz  12593  bezoutlembi  12594  bezoutlemle  12597  bezoutlemsup  12598  mulgcd  12605  gcdzeq  12611  dvdsmulgcd  12614  sqgcd  12618  bezoutr1  12622  nninfctlemfo  12629  algcvga  12641  algfx  12642  eucalglt  12647  eucalg  12649  lcmneg  12664  lcmabs  12666  lcmgcdlem  12667  ncoprmgcdne1b  12679  mulgcddvds  12684  qredeq  12686  divgcdcoprm0  12691  cncongr1  12693  isprm2lem  12706  nprm  12713  dvdsnprmd  12715  prmdvdsfz  12729  isprm5lem  12731  coprm  12734  isprm6  12737  sqrt2irr  12752  pw2dvdslemn  12755  pw2dvdseulemle  12757  oddpwdclemdvds  12760  oddpwdclemndvds  12761  sqrt2irrap  12770  qnumdencl  12777  prmdiv  12825  modprmn0modprm0  12847  prm23lt5  12854  pythagtriplem4  12859  pythagtriplem19  12873  pythagtrip  12874  pclemub  12878  pcpre1  12883  pcpremul  12884  pceulem  12885  pcqcl  12897  pcidlem  12914  pcgcd1  12919  pc2dvds  12921  dvdsprmpweqle  12928  difsqpwdvds  12929  pcadd  12931  pcmpt  12934  expnprm  12944  pockthg  12948  infpnlem2  12951  prmunb  12953  1arith  12958  4sqlem10  12978  4sqlem11  12992  4sqlem12  12993  4sqlem13m  12994  4sqlem17  12998  4sqlem18  12999  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemrnh  13055  ennnfonelemnn0  13061  ennnfonelemim  13063  exmidunben  13065  ctinfomlemom  13066  ctinfom  13067  ctinf  13069  omctfn  13082  nninfdclemp1  13089  setscomd  13141  imasaddfnlemg  13415  mhmf1o  13571  grpinveu  13639  grpasscan1  13664  dfgrp3mlem  13699  grp1inv  13708  issubg4m  13798  ghmf1o  13880  srgisid  14018  ringadd2  14059  ringinvnzdiv  14082  unitgrp  14149  ringelnzr  14220  lringuplu  14229  subrguss  14269  subrgintm  14276  aprcotr  14318  islmodd  14326  lssclg  14397  lss0cl  14402  lssvneln0  14406  lss1d  14416  lmodindp1  14461  rnglidlmmgm  14529  znidomb  14691  znunit  14692  znrrg  14693  mplsubgfilemcl  14732  mplsubgfileminv  14733  tgcl  14807  neii1  14890  neii2  14892  neiss  14893  tpnei  14903  tgrest  14912  ssrest  14925  icnpimaex  14954  lmcvg  14960  cnpnei  14962  cnptopco  14965  lmff  14992  txcnp  15014  txcn  15018  hmeontr  15056  blssec  15181  mopni3  15227  blsscls2  15236  comet  15242  bdxmet  15244  bdmopn  15247  xmettxlem  15252  xmettx  15253  addcncntoplem  15304  mpomulcn  15309  mulc1cncf  15332  cncfco  15334  cncfmptc  15339  mulcncflem  15350  mulcncf  15351  dedekindeulemlu  15364  dedekindeulemeu  15365  suplociccreex  15367  suplociccex  15368  dedekindicclemlu  15373  dedekindicclemeu  15374  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemloc  15384  ivthinc  15386  ivthreinc  15388  ivthdichlem  15394  limcimolemlt  15407  limcresi  15409  cnplimcim  15410  cnplimclemle  15411  cnplimclemr  15412  limccnpcntop  15418  limccoap  15421  dvcoapbr  15450  dvcj  15452  plyf  15480  plyaddlem1  15490  plymullem1  15491  plyco  15502  plycj  15504  plycn  15505  plyrecj  15506  dvply2g  15509  efltlemlt  15517  sin0pilem2  15525  tangtx  15581  logdivlti  15624  rplogbval  15688  logbgcd1irraplemexp  15711  logbgcd1irraplemap  15712  logbgcd1irrap  15713  perfect1  15741  perfectlem1  15742  perfectlem2  15743  lgsval4a  15770  lgsdir2lem3  15778  lgsne0  15786  gausslemma2dlem3  15811  gausslemma2dlem4  15812  gausslemma2dlem6  15815  gausslemma2dlem7  15816  gausslemma2d  15817  lgseisenlem1  15818  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem2  15830  lgsquad3  15832  2lgsoddprmlem2  15854  2sqlem8a  15870  2sqlem8  15871  2sqlem9  15872  lpvtx  15949  upgrex  15973  upgr1een  15994  edgupgren  16011  umgredg  16015  upgrpredgv  16016  upgredg2vtx  16018  upgredgpr  16019  uspgrf1oedg  16046  usgredg4  16085  uspgredgdomord  16099  usgr1vr  16118  wlkvtxiedg  16215  wlkvtxiedgg  16216  wlk1walkdom  16229  upgriswlkdc  16230  upgrwlkedg  16231  uspgr2wlkeq  16235  uspgr2wlkeqi  16237  umgrwlknloop  16238  eupth2lem2dc  16329  trlsegvdeglem1  16330  eupth2lem3lem4fi  16343  bj-exlimmpi  16417  uzdcinzz  16445  bj-charfundcALT  16455  bj-2inf  16584  bj-peano4  16601  bj-nn0suc  16610  pw1ndom3  16640  subctctexmid  16652  nninfalllem1  16661  nninfsellemqall  16668  nninfomnilem  16671  nninffeq  16673  nnnninfex  16675  exmidsbthrlem  16677  sbthomlem  16680  refeq  16683  isomninnlem  16685  apdifflemr  16702  redcwlpo  16711  reap0  16714  nconstwlpolem  16721