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  146  mpbird  166  jcai  309  mp2and  431  pm2.21dd  615  mt2d  620  mpjaod  713  stdcndcOLD  841  impidc  853  jadc  858  pm2.54dc  886  pm4.55dc  933  oplem1  970  mp3and  1335  xor3dc  1382  exlimdd  1865  exlimddv  1891  eqrdav  2169  necon1aidc  2391  necon1bidc  2392  necon4aidc  2408  reximddv  2573  reximssdv  2574  rexlimddv  2592  vtoclgft  2780  rspcedvd  2840  sseldd  3148  ssneldd  3150  tpid3g  3696  preq12b  3755  axpweq  4155  exmid1dc  4184  opth  4220  issod  4302  frirrg  4333  frind  4335  ralxfr2d  4447  rexxfr2d  4448  eldifpw  4460  onun2  4472  onuni  4476  elirr  4523  en2lp  4536  wetriext  4559  peano2  4577  relop  4759  elres  4925  sotri2  5006  iota4an  5177  iota5  5178  funeu  5221  funopg  5230  imadiflem  5275  funimaexglem  5279  ssimaex  5555  ffvelrn  5627  dff3im  5639  dffo4  5642  f1eqcocnv  5768  f1oiso2  5804  riota5f  5831  riotass2  5833  acexmidlemcase  5846  ovmpodf  5982  ovmpodv2  5984  ovi3  5987  ov6g  5988  caoftrn  6084  op1steq  6156  tfr0dm  6299  tfrlemibxssdm  6304  tfrlemi14d  6310  tfr1onlembxssdm  6320  tfr1onlemaccex  6325  tfr1onlemres  6326  tfrcllembxssdm  6333  tfrcllemaccex  6338  tfrcllemres  6339  rdgivallem  6358  nnsucelsuc  6468  nnsucsssuc  6469  dcdifsnid  6481  nnawordex  6506  ersym  6523  mapvalg  6634  pmvalg  6635  mapsn  6666  fundmen  6782  mapdom1g  6823  fidceq  6845  fin0or  6862  findcard2  6865  findcard2s  6866  fiintim  6904  suplub2ti  6976  supsnti  6980  supisoex  6984  difinfsnlem  7074  difinfsn  7075  ctm  7084  ctssdclemn0  7085  ctssdccl  7086  ctssdc  7088  enumctlemm  7089  nnnninfeq2  7103  enomnilem  7112  exmidomniim  7115  exmidomni  7116  fodjuomnilemdc  7118  fodjuomnilemres  7122  omnimkv  7130  mkvprop  7132  omniwomnimkv  7141  en2eleq  7165  acfun  7177  exmidontriimlem1  7191  exmidontriimlem4  7194  exmidontriim  7195  ccfunen  7219  cc4f  7224  cc4n  7226  elni2  7269  mulclpi  7283  nlt1pig  7296  indpi  7297  recclnq  7347  ltexnqq  7363  halfnqq  7365  prarloclemarch  7373  prarloclemarch2  7374  prop  7430  prltlu  7442  prarloclem3step  7451  prarloclem5  7455  prarloclem  7456  prarloc  7458  prarloc2  7459  genpml  7472  genpmu  7473  genprndl  7476  genprndu  7477  genpdisj  7478  addnqprllem  7482  addnqprulem  7483  addlocprlemeq  7488  addlocprlemgt  7489  addlocprlem  7490  addlocpr  7491  nqprloc  7500  nqprl  7506  nqpru  7507  addnqprlemrl  7512  addnqprlemru  7513  appdivnq  7518  prmuloc  7521  prmuloc2  7522  mullocprlem  7525  mullocpr  7526  mulnqprlemrl  7528  mulnqprlemru  7529  ltprordil  7544  ltpopr  7550  ltsopr  7551  ltaddpr  7552  ltexprlemm  7555  ltexprlemopl  7556  ltexprlemlol  7557  ltexprlemopu  7558  ltexprlemupu  7559  ltexprlemloc  7562  ltexprlemfl  7564  ltexprlemrl  7565  ltexprlemfu  7566  ltexprlemru  7567  ltaprg  7574  recexprlemm  7579  recexprlem1ssl  7588  recexprlem1ssu  7589  aptiprleml  7594  aptiprlemu  7595  archpr  7598  cauappcvgprlemm  7600  cauappcvgprlemopl  7601  cauappcvgprlemlol  7602  cauappcvgprlemopu  7603  cauappcvgprlemupu  7604  cauappcvgprlemdisj  7606  cauappcvgprlemloc  7607  cauappcvgprlemladdfu  7609  cauappcvgprlemladdfl  7610  cauappcvgprlemladdru  7611  cauappcvgprlem1  7614  archrecpr  7619  caucvgprlemnkj  7621  caucvgprlemnbj  7622  caucvgprlemm  7623  caucvgprlemopl  7624  caucvgprlemlol  7625  caucvgprlemopu  7626  caucvgprlemupu  7627  caucvgprlemdisj  7629  caucvgprlemloc  7630  caucvgprlemladdfu  7632  caucvgprlem1  7634  caucvgprlemlim  7636  caucvgprprlemnbj  7648  caucvgprprlemml  7649  caucvgprprlemopl  7652  caucvgprprlemlol  7653  caucvgprprlemopu  7654  caucvgprprlemupu  7655  caucvgprprlemdisj  7657  caucvgprprlemloc  7658  caucvgprprlemexbt  7661  caucvgprprlemaddq  7663  caucvgprprlemlim  7666  suplocexprlemss  7670  suplocexprlemrl  7672  suplocexprlemmu  7673  suplocexprlemru  7674  suplocexprlemdisj  7675  suplocexprlemloc  7676  suplocexprlemub  7678  suplocexprlemlub  7679  recexgt0sr  7728  mulgt0sr  7733  archsr  7737  caucvgsrlemoffcau  7753  suplocsrlemb  7761  suplocsrlempr  7762  suplocsrlem  7763  cnm  7787  axarch  7846  axcaucvglemcau  7853  axpre-suploclemres  7856  lelttr  8001  ltletr  8002  ltled  8031  cnegexlem1  8087  cnegexlem2  8088  renegcl  8173  negf1o  8294  gt0add  8485  apreap  8499  apirr  8517  apsym  8518  apcotr  8519  apadd1  8520  apneg  8523  mulext1  8524  mulap0r  8527  apti  8534  aprcl  8558  recexap  8564  mulap0  8565  receuap  8580  mul0eqap  8581  lep1  8754  lem1  8756  letrp1  8757  recreclt  8809  lbinf  8857  suprubex  8860  nnrecgt0  8909  bndndx  9127  nn0ge2m1nn  9188  elnn0z  9218  peano2z  9241  zaddcl  9245  ztri3or0  9247  zltnle  9251  zdceq  9280  zdcle  9281  zdclt  9282  zdiv  9293  zeo  9310  fnn0ind  9321  btwnz  9324  uzm1  9510  uzp1  9513  indstr  9545  supinfneg  9547  infsupneg  9548  eluzdc  9562  nn01to3  9569  qapne  9591  xrltled  9749  xrlelttr  9756  xrltletr  9757  ge0nemnf  9774  fzdcel  9989  elfzouz2  10110  fzoss1  10120  fzospliti  10125  fzocatel  10148  fzostep1  10186  qtri3or  10192  qltnle  10195  qdceq  10196  exbtwnzlemex  10199  rebtwn2zlemstep  10202  rebtwn2z  10204  qbtwnxr  10207  ioom  10210  ico0  10211  ioc0  10212  flqeqceilz  10267  modqadd1  10310  modqmul1  10326  frec2uzuzd  10351  frec2uzlt2d  10353  frec2uzf1od  10355  frecuzrdgrrn  10357  frec2uzrdg  10358  frecuzrdgrcl  10359  frecuzrdgsuc  10363  frecuzrdgrclt  10364  frecuzrdgdomlem  10366  uzsinds  10391  seqvalcd  10408  seqovcd  10412  seq3fveq2  10418  seq3shft2  10422  monoord  10425  seq3split  10428  seq3caopr3  10430  iseqf1olemab  10438  iseqf1olemnanb  10439  iseqf1olemqk  10443  seq3id3  10456  seq3id2  10458  seq3homo  10459  expgt1  10507  m1expeven  10516  expnbnd  10592  expnlbnd2  10594  nn0ltexp2  10637  apexp1  10645  hashennn  10707  zfz1isolem1  10768  seq3coll  10770  cjap  10863  caucvgre  10938  cvg1nlemres  10942  resqrexlemgt0  10977  resqrexlemglsq  10979  resqrexlemga  10980  resqrtcl  10986  abslt  11045  abssubap0  11047  abssubne0  11048  caubnd2  11074  qdenre  11159  maxabslemlub  11164  maxabs  11166  maxleast  11170  fimaxre2  11183  xrmaxiflemlub  11204  xrmaxif  11207  xrmaxltsup  11214  xrmaxadd  11217  xrmineqinf  11225  climuni  11249  2clim  11257  climcn1  11264  climcn2  11265  subcn2  11267  mulcn2  11268  climsqz  11291  climsqz2  11292  climcau  11303  climcvg1nlem  11305  climcaucn  11307  serf0  11308  sumrbdclem  11333  summodclem2  11338  zsumdc  11340  divcnv  11453  absltap  11465  absgtap  11466  mertenslem2  11492  ntrivcvgap  11504  prodrbdclem  11527  prodmodclem2  11533  zproddc  11535  prodssdc  11545  fprodsplitdc  11552  fprodcl2lem  11561  efcllemp  11614  tanvalap  11664  sin01bnd  11713  cos01bnd  11714  sin01gt0  11717  absef  11725  eirrap  11733  dvds0  11761  dvdsmul1  11768  dvdsmultr1d  11787  dvdslelemd  11796  divconjdvds  11802  alzdvds  11807  sqoddm1div8z  11838  nno  11858  divalglemex  11874  zsupcllemstep  11893  zsupcl  11895  infssuzledc  11898  dvdsbnd  11904  dvdslegcd  11912  zeqzmulgcd  11918  gcd0id  11927  gcdaddm  11932  gcd1  11935  gcdabs  11936  bezoutlemnewy  11944  bezoutlemstep  11945  bezoutlemmain  11946  bezoutlemex  11949  bezoutlemzz  11950  bezoutlemaz  11951  bezoutlembz  11952  bezoutlembi  11953  bezoutlemle  11956  bezoutlemsup  11957  mulgcd  11964  gcdzeq  11970  dvdsmulgcd  11973  sqgcd  11977  bezoutr1  11981  algcvga  11998  algfx  11999  eucalglt  12004  eucalg  12006  lcmneg  12021  lcmabs  12023  lcmgcdlem  12024  ncoprmgcdne1b  12036  mulgcddvds  12041  qredeq  12043  divgcdcoprm0  12048  cncongr1  12050  isprm2lem  12063  nprm  12070  dvdsnprmd  12072  prmdvdsfz  12086  isprm5lem  12088  coprm  12091  isprm6  12094  sqrt2irr  12109  pw2dvdslemn  12112  pw2dvdseulemle  12114  oddpwdclemdvds  12117  oddpwdclemndvds  12118  sqrt2irrap  12127  qnumdencl  12134  prmdiv  12182  modprmn0modprm0  12203  prm23lt5  12210  pythagtriplem4  12215  pythagtriplem19  12229  pythagtrip  12230  pclemub  12234  pcpre1  12239  pcpremul  12240  pceulem  12241  pcqcl  12253  pcidlem  12269  pcgcd1  12274  pc2dvds  12276  dvdsprmpweqle  12283  difsqpwdvds  12284  pcadd  12286  pcmpt  12288  expnprm  12298  pockthg  12302  infpnlem2  12305  prmunb  12307  1arith  12312  4sqlem10  12332  ennnfonelemex  12362  ennnfonelemhom  12363  ennnfonelemrnh  12364  ennnfonelemnn0  12370  ennnfonelemim  12372  exmidunben  12374  ctinfomlemom  12375  ctinfom  12376  ctinf  12378  omctfn  12391  nninfdclemp1  12398  mhmf1o  12686  grpinveu  12734  tgcl  12823  neii1  12906  neii2  12908  neiss  12909  tpnei  12919  tgrest  12928  ssrest  12941  icnpimaex  12970  lmcvg  12976  cnpnei  12978  cnptopco  12981  lmff  13008  txcnp  13030  txcn  13034  hmeontr  13072  blssec  13197  mopni3  13243  blsscls2  13252  comet  13258  bdxmet  13260  bdmopn  13263  xmettxlem  13268  xmettx  13269  addcncntoplem  13310  mulc1cncf  13335  cncfco  13337  cncfmptc  13341  mulcncflem  13349  mulcncf  13350  dedekindeulemlu  13358  dedekindeulemeu  13359  suplociccreex  13361  suplociccex  13362  dedekindicclemlu  13367  dedekindicclemeu  13368  ivthinclemlopn  13373  ivthinclemlr  13374  ivthinclemuopn  13375  ivthinclemur  13376  ivthinclemloc  13378  ivthinc  13380  limcimolemlt  13392  limcresi  13394  cnplimcim  13395  cnplimclemle  13396  cnplimclemr  13397  limccnpcntop  13403  limccoap  13406  dvcoapbr  13430  dvcj  13432  efltlemlt  13454  sin0pilem2  13462  tangtx  13518  logdivlti  13561  rplogbval  13622  logbgcd1irraplemexp  13645  logbgcd1irraplemap  13646  logbgcd1irrap  13647  lgsval4a  13682  lgsdir2lem3  13690  lgsne0  13698  2sqlem8a  13717  2sqlem8  13718  2sqlem9  13719  bj-exlimmpi  13770  uzdcinzz  13798  bj-charfundcALT  13809  bj-2inf  13938  bj-peano4  13955  bj-nn0suc  13964  exmid1stab  13998  subctctexmid  13999  nninfalllem1  14006  nninfsellemqall  14013  nninfomnilem  14016  nninffeq  14018  exmidsbthrlem  14019  sbthomlem  14022  refeq  14025  isomninnlem  14027  apdifflemr  14044  redcwlpo  14052  reap0  14055  nconstwlpolem  14061