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  5829  f1eqcocnv  5931  f1oiso2  5967  riota5f  5997  riotass2  5999  acexmidlemcase  6012  elovimad  6061  ovmpodf  6152  ovmpodv2  6154  ovi3  6158  ov6g  6159  caoftrn  6267  op1steq  6341  tfr0dm  6487  tfrlemibxssdm  6492  tfrlemi14d  6498  tfr1onlembxssdm  6508  tfr1onlemaccex  6513  tfr1onlemres  6514  tfrcllembxssdm  6521  tfrcllemaccex  6526  tfrcllemres  6527  rdgivallem  6546  nnsucelsuc  6658  nnsucsssuc  6659  dcdifsnid  6671  nnawordex  6696  ersym  6713  mapvalg  6826  pmvalg  6827  mapsn  6858  fundmen  6980  1dom1el  6992  en2  6997  pw2f1odclem  7019  mapdom1g  7032  fidceq  7055  fin0or  7074  findcard2  7077  findcard2s  7078  fidcen  7087  prfidceq  7119  fiintim  7122  suplub2ti  7199  supsnti  7203  supisoex  7207  difinfsnlem  7297  difinfsn  7298  ctm  7307  ctssdclemn0  7308  ctssdccl  7309  ctssdc  7311  enumctlemm  7312  nninfninc  7321  nnnninfeq2  7327  enomnilem  7336  exmidomniim  7339  exmidomni  7340  fodjuomnilemdc  7342  fodjuomnilemres  7346  omnimkv  7354  mkvprop  7356  omniwomnimkv  7365  en2prde  7397  pr2cv1  7399  en2eleq  7405  acfun  7421  exmidontriimlem1  7435  exmidontriimlem4  7438  exmidontriim  7439  ccfunen  7482  cc4f  7487  cc4n  7489  elni2  7533  mulclpi  7547  nlt1pig  7560  indpi  7561  recclnq  7611  ltexnqq  7627  halfnqq  7629  prarloclemarch  7637  prarloclemarch2  7638  prop  7694  prltlu  7706  prarloclem3step  7715  prarloclem5  7719  prarloclem  7720  prarloc  7722  prarloc2  7723  genpml  7736  genpmu  7737  genprndl  7740  genprndu  7741  genpdisj  7742  addnqprllem  7746  addnqprulem  7747  addlocprlemeq  7752  addlocprlemgt  7753  addlocprlem  7754  addlocpr  7755  nqprloc  7764  nqprl  7770  nqpru  7771  addnqprlemrl  7776  addnqprlemru  7777  appdivnq  7782  prmuloc  7785  prmuloc2  7786  mullocprlem  7789  mullocpr  7790  mulnqprlemrl  7792  mulnqprlemru  7793  ltprordil  7808  ltpopr  7814  ltsopr  7815  ltaddpr  7816  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  ltexprlemloc  7826  ltexprlemfl  7828  ltexprlemrl  7829  ltexprlemfu  7830  ltexprlemru  7831  ltaprg  7838  recexprlemm  7843  recexprlem1ssl  7852  recexprlem1ssu  7853  aptiprleml  7858  aptiprlemu  7859  archpr  7862  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemupu  7868  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  cauappcvgprlem1  7878  archrecpr  7883  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemupu  7891  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprlem1  7898  caucvgprlemlim  7900  caucvgprprlemnbj  7912  caucvgprprlemml  7913  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemupu  7919  caucvgprprlemdisj  7921  caucvgprprlemloc  7922  caucvgprprlemexbt  7925  caucvgprprlemaddq  7927  caucvgprprlemlim  7930  suplocexprlemss  7934  suplocexprlemrl  7936  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  suplocexprlemlub  7943  recexgt0sr  7992  mulgt0sr  7997  archsr  8001  caucvgsrlemoffcau  8017  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  cnm  8051  axarch  8110  axcaucvglemcau  8117  axpre-suploclemres  8120  lelttr  8267  ltletr  8268  ltled  8297  cnegexlem1  8353  cnegexlem2  8354  renegcl  8439  negf1o  8560  gt0add  8752  apreap  8766  apirr  8784  apsym  8785  apcotr  8786  apadd1  8787  apneg  8790  mulext1  8791  mulap0r  8794  apti  8801  aprcl  8825  aptap  8829  recexap  8832  mulap0  8833  receuap  8848  mul0eqap  8849  lep1  9024  lem1  9026  letrp1  9027  recreclt  9079  lbinf  9127  suprubex  9130  nnrecgt0  9180  bndndx  9400  nn0ge2m1nn  9461  elnn0z  9491  peano2z  9514  zaddcl  9518  ztri3or0  9520  zltnle  9524  zdceq  9554  zdcle  9555  zdclt  9556  zdiv  9567  zeo  9584  fnn0ind  9595  btwnz  9598  uzm1  9786  uzp1  9789  indstr  9826  supinfneg  9828  infsupneg  9829  eluzdc  9843  nn01to3  9850  qapne  9872  xrltled  10033  xrlelttr  10040  xrltletr  10041  ge0nemnf  10058  fzdcel  10274  elfzouz2  10396  fzoss1  10407  fzospliti  10412  elincfzoext  10437  fzocatel  10443  fzostep1  10482  zsupcllemstep  10488  zsupcl  10490  infssuzledc  10493  qtri3or  10499  qltnle  10502  qdceq  10503  qdclt  10504  exbtwnzlemex  10508  rebtwn2zlemstep  10511  rebtwn2z  10513  qbtwnxr  10516  ioom  10519  ico0  10520  ioc0  10521  flqeqceilz  10579  modqadd1  10622  modqmul1  10638  frec2uzuzd  10663  frec2uzlt2d  10665  frec2uzf1od  10667  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgdomlem  10678  uzsinds  10705  seqvalcd  10722  seqovcd  10728  seq3fveq2  10736  seqfveq2g  10738  seq3shft2  10742  seqshft2g  10743  monoord  10746  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  iseqf1olemab  10763  iseqf1olemnanb  10764  iseqf1olemqk  10768  seqf1oglem1  10780  seqf1og  10782  seq3id3  10785  seq3id2  10787  seq3homo  10788  seqhomog  10791  expgt1  10838  m1expeven  10847  expnbnd  10924  expnlbnd2  10926  nn0ltexp2  10970  apexp1  10979  hashennn  11041  zfz1isolem1  11103  seq3coll  11105  pfxwrdsymbg  11270  wrdind  11302  wrd2ind  11303  cjap  11466  caucvgre  11541  cvg1nlemres  11545  resqrexlemgt0  11580  resqrexlemglsq  11582  resqrexlemga  11583  resqrtcl  11589  abslt  11648  abssubap0  11650  abssubne0  11651  caubnd2  11677  qdenre  11762  maxabslemlub  11767  maxabs  11769  maxleast  11773  fimaxre2  11787  xrmaxiflemlub  11808  xrmaxif  11811  xrmaxltsup  11818  xrmaxadd  11821  xrmineqinf  11829  climuni  11853  2clim  11861  climcn1  11868  climcn2  11869  subcn2  11871  mulcn2  11872  climsqz  11895  climsqz2  11896  climcau  11907  climcvg1nlem  11909  climcaucn  11911  serf0  11912  sumrbdclem  11937  summodclem2  11942  zsumdc  11944  divcnv  12057  absltap  12069  absgtap  12070  mertenslem2  12096  ntrivcvgap  12108  prodrbdclem  12131  prodmodclem2  12137  zproddc  12139  prodssdc  12149  fprodsplitdc  12156  fprodcl2lem  12165  efcllemp  12218  tanvalap  12268  sin01bnd  12317  cos01bnd  12318  sin01gt0  12322  absef  12330  eirrap  12338  dvds0  12366  dvdsmul1  12373  dvdsmultr1d  12392  dvdslelemd  12403  divconjdvds  12409  alzdvds  12414  3dvds  12424  sqoddm1div8z  12446  nno  12466  divalglemex  12482  bits0o  12510  dvdsbnd  12526  dvdslegcd  12534  zeqzmulgcd  12540  gcd0id  12549  gcdaddm  12554  gcd1  12557  gcdabs  12558  bezoutlemnewy  12566  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlemex  12571  bezoutlemzz  12572  bezoutlemaz  12573  bezoutlembz  12574  bezoutlembi  12575  bezoutlemle  12578  bezoutlemsup  12579  mulgcd  12586  gcdzeq  12592  dvdsmulgcd  12595  sqgcd  12599  bezoutr1  12603  nninfctlemfo  12610  algcvga  12622  algfx  12623  eucalglt  12628  eucalg  12630  lcmneg  12645  lcmabs  12647  lcmgcdlem  12648  ncoprmgcdne1b  12660  mulgcddvds  12665  qredeq  12667  divgcdcoprm0  12672  cncongr1  12674  isprm2lem  12687  nprm  12694  dvdsnprmd  12696  prmdvdsfz  12710  isprm5lem  12712  coprm  12715  isprm6  12718  sqrt2irr  12733  pw2dvdslemn  12736  pw2dvdseulemle  12738  oddpwdclemdvds  12741  oddpwdclemndvds  12742  sqrt2irrap  12751  qnumdencl  12758  prmdiv  12806  modprmn0modprm0  12828  prm23lt5  12835  pythagtriplem4  12840  pythagtriplem19  12854  pythagtrip  12855  pclemub  12859  pcpre1  12864  pcpremul  12865  pceulem  12866  pcqcl  12878  pcidlem  12895  pcgcd1  12900  pc2dvds  12902  dvdsprmpweqle  12909  difsqpwdvds  12910  pcadd  12912  pcmpt  12915  expnprm  12925  pockthg  12929  infpnlem2  12932  prmunb  12934  1arith  12939  4sqlem10  12959  4sqlem11  12973  4sqlem12  12974  4sqlem13m  12975  4sqlem17  12979  4sqlem18  12980  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemrnh  13036  ennnfonelemnn0  13042  ennnfonelemim  13044  exmidunben  13046  ctinfomlemom  13047  ctinfom  13048  ctinf  13050  omctfn  13063  nninfdclemp1  13070  setscomd  13122  imasaddfnlemg  13396  mhmf1o  13552  grpinveu  13620  grpasscan1  13645  dfgrp3mlem  13680  grp1inv  13689  issubg4m  13779  ghmf1o  13861  srgisid  13998  ringadd2  14039  ringinvnzdiv  14062  unitgrp  14129  ringelnzr  14200  lringuplu  14209  subrguss  14249  subrgintm  14256  aprcotr  14298  islmodd  14306  lssclg  14377  lss0cl  14382  lssvneln0  14386  lss1d  14396  lmodindp1  14441  rnglidlmmgm  14509  znidomb  14671  znunit  14672  znrrg  14673  mplsubgfilemcl  14712  mplsubgfileminv  14713  tgcl  14787  neii1  14870  neii2  14872  neiss  14873  tpnei  14883  tgrest  14892  ssrest  14905  icnpimaex  14934  lmcvg  14940  cnpnei  14942  cnptopco  14945  lmff  14972  txcnp  14994  txcn  14998  hmeontr  15036  blssec  15161  mopni3  15207  blsscls2  15216  comet  15222  bdxmet  15224  bdmopn  15227  xmettxlem  15232  xmettx  15233  addcncntoplem  15284  mpomulcn  15289  mulc1cncf  15312  cncfco  15314  cncfmptc  15319  mulcncflem  15330  mulcncf  15331  dedekindeulemlu  15344  dedekindeulemeu  15345  suplociccreex  15347  suplociccex  15348  dedekindicclemlu  15353  dedekindicclemeu  15354  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemloc  15364  ivthinc  15366  ivthreinc  15368  ivthdichlem  15374  limcimolemlt  15387  limcresi  15389  cnplimcim  15390  cnplimclemle  15391  cnplimclemr  15392  limccnpcntop  15398  limccoap  15401  dvcoapbr  15430  dvcj  15432  plyf  15460  plyaddlem1  15470  plymullem1  15471  plyco  15482  plycj  15484  plycn  15485  plyrecj  15486  dvply2g  15489  efltlemlt  15497  sin0pilem2  15505  tangtx  15561  logdivlti  15604  rplogbval  15668  logbgcd1irraplemexp  15691  logbgcd1irraplemap  15692  logbgcd1irrap  15693  perfect1  15721  perfectlem1  15722  perfectlem2  15723  lgsval4a  15750  lgsdir2lem3  15758  lgsne0  15766  gausslemma2dlem3  15791  gausslemma2dlem4  15792  gausslemma2dlem6  15795  gausslemma2dlem7  15796  gausslemma2d  15797  lgseisenlem1  15798  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem2  15810  lgsquad3  15812  2lgsoddprmlem2  15834  2sqlem8a  15850  2sqlem8  15851  2sqlem9  15852  lpvtx  15929  upgrex  15953  upgr1een  15974  edgupgren  15991  umgredg  15995  upgrpredgv  15996  upgredg2vtx  15998  upgredgpr  15999  uspgrf1oedg  16026  usgredg4  16065  uspgredgdomord  16079  usgr1vr  16098  wlkvtxiedg  16195  wlkvtxiedgg  16196  wlk1walkdom  16209  upgriswlkdc  16210  upgrwlkedg  16211  uspgr2wlkeq  16215  uspgr2wlkeqi  16217  umgrwlknloop  16218  eupth2lem2dc  16309  trlsegvdeglem1  16310  bj-exlimmpi  16366  uzdcinzz  16394  bj-charfundcALT  16404  bj-2inf  16533  bj-peano4  16550  bj-nn0suc  16559  pw1ndom3  16589  subctctexmid  16601  nninfalllem1  16610  nninfsellemqall  16617  nninfomnilem  16620  nninffeq  16622  nnnninfex  16624  exmidsbthrlem  16626  sbthomlem  16629  refeq  16632  isomninnlem  16634  apdifflemr  16651  redcwlpo  16659  reap0  16662  nconstwlpolem  16669