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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-2 7

This theorem is used 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  437  pm2.21dd  629  mt2d  634  mpnanrd  704  mpjaod  730  stdcndcOLD  858  impidc  870  jadc  875  pm2.54dc  903  oplem1  988  mp3and  1381  xor3dc  1436  exlimdd  1925  exlimddv  1954  eqrdav  2237  necon1aidc  2471  necon1bidc  2472  necon4aidc  2488  reximddv  2653  reximssdv  2654  rexlimddv  2673  vtoclgft  2873  rspcedvd  2935  sseldd  3249  ssneldd  3251  tpid3g  3828  preq12b  3895  axpweq  4308  exmid1dc  4337  exmid1stab  4345  opth  4377  issod  4464  frirrg  4495  frind  4497  ralxfr2d  4610  rexxfr2d  4611  eldifpw  4623  onun2  4637  onuni  4641  elirr  4688  en2lp  4701  wetriext  4724  peano2  4742  relop  4930  elres  5099  sotri2  5185  iota4an  5358  iota5  5359  funeu  5402  funopg  5411  imadiflem  5460  funimaexglem  5464  ssimaex  5764  ffvelcdm  5841  dff3im  5853  dffo4  5856  funopsn  5891  f1eqcocnv  5997  f1oiso2  6033  riota5f  6065  riotass2  6067  acexmidlemcase  6080  elovimad  6129  ovmpodf  6220  ovmpodv2  6222  ovi3  6226  ov6g  6227  caoftrn  6335  op1steq  6413  fvdifsuppst  6484  suppssdc  6500  suppofss1dcl  6504  suppofss2dcl  6505  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemi14d  6604  tfr1onlembxssdm  6614  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllembxssdm  6627  tfrcllemaccex  6632  tfrcllemres  6633  rdgivallem  6652  nnsucelsuc  6764  nnsucsssuc  6765  dcdifsnid  6777  nnawordex  6802  ersym  6819  mapvalg  6932  pmvalg  6933  mapsnd  6970  mapsn  6972  fundmen  7094  1dom1el  7107  en2  7112  pw2f1odclem  7134  mapdom1g  7147  fidceq  7171  fin0or  7190  findcard2  7193  findcard2s  7194  fidcen  7203  prfidceq  7235  fiintim  7238  suplub2ti  7342  supsnti  7346  supisoex  7350  difinfsnlem  7440  difinfsn  7441  ctm  7450  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  enumctlemm  7455  nninfninc  7464  nnnninfeq2  7470  enomnilem  7479  exmidomniim  7482  exmidomni  7483  fodjuomnilemdc  7485  fodjuomnilemres  7489  omnimkv  7497  mkvprop  7499  omniwomnimkv  7508  en2prde  7540  pr2cv1  7542  en2eleq  7548  acfun  7564  exmidontriimlem1  7578  exmidontriimlem4  7581  exmidontriim  7582  papsym  7613  papcotr  7614  ccfunen  7631  cc4f  7636  cc4n  7638  elni2  7682  mulclpi  7696  nlt1pig  7709  indpi  7710  recclnq  7760  ltexnqq  7776  halfnqq  7778  prarloclemarch  7786  prarloclemarch2  7787  prop  7843  prltlu  7855  prarloclem3step  7864  prarloclem5  7868  prarloclem  7869  prarloc  7871  prarloc2  7872  genpml  7885  genpmu  7886  genprndl  7889  genprndu  7890  genpdisj  7891  addnqprllem  7895  addnqprulem  7896  addlocprlemeq  7901  addlocprlemgt  7902  addlocprlem  7903  addlocpr  7904  nqprloc  7913  nqprl  7919  nqpru  7920  addnqprlemrl  7925  addnqprlemru  7926  appdivnq  7931  prmuloc  7934  prmuloc2  7935  mullocprlem  7938  mullocpr  7939  mulnqprlemrl  7941  mulnqprlemru  7942  ltprordil  7957  ltpopr  7963  ltsopr  7964  ltaddpr  7965  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  ltaprg  7987  recexprlemm  7992  recexprlem1ssl  8001  recexprlem1ssu  8002  aptiprleml  8007  aptiprlemu  8008  archpr  8011  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlem1  8027  archrecpr  8032  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprlem1  8047  caucvgprlemlim  8049  caucvgprprlemnbj  8061  caucvgprprlemml  8062  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemupu  8068  caucvgprprlemdisj  8070  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  caucvgprprlemaddq  8076  caucvgprprlemlim  8079  suplocexprlemss  8083  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  recexgt0sr  8141  mulgt0sr  8146  archsr  8150  caucvgsrlemoffcau  8166  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  cnm  8200  axarch  8259  axcaucvglemcau  8266  axpre-suploclemres  8269  lelttr  8415  ltletr  8416  ltled  8447  cnegexlem1  8503  cnegexlem2  8504  renegcl  8589  negf1o  8711  gt0add  8904  apreap  8918  apirr  8936  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  mulap0r  8946  apti  8953  aprcl  8977  aptap  8981  recexap  8984  mulap0  8985  receuap  9002  mul0eqap  9003  lep1  9178  lem1  9180  letrp1  9181  recreclt  9233  lbinf  9281  suprubex  9284  nnrecgt0  9345  bndndx  9567  nn0ge2m1nn  9632  elnn0z  9662  peano2z  9685  zaddcl  9689  ztri3or0  9691  zltnle  9695  zdceq  9725  zdcle  9726  zdclt  9727  zdiv  9739  zeo  9756  fnn0ind  9767  btwnz  9770  uzm1  9963  uzp1  9966  indstr  10003  supinfneg  10005  infsupneg  10006  eluzdc  10020  nn01to3  10027  qapne  10049  xrltled  10212  xrlelttr  10219  xrltletr  10220  ge0nemnf  10237  fzdcel  10455  elfzouz2  10580  fzoss1  10591  fzospliti  10596  elincfzoext  10622  fzocatel  10628  fzostep1  10667  zsupcllemstep  10673  zsupcl  10675  infssuzledc  10678  qtri3or  10686  qltnle  10689  qdceq  10690  qdclt  10691  exbtwnzlemex  10695  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnxr  10703  ioom  10706  ico0  10707  ioc0  10708  flqeqceilz  10770  modqadd1  10813  modqmul1  10829  frec2uzuzd  10854  frec2uzlt2d  10856  frec2uzf1od  10858  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgdomlem  10869  uzsinds  10896  seqvalcd  10913  seqovcd  10919  seq3fveq2  10927  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  monoord  10937  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  iseqf1olemab  10954  iseqf1olemnanb  10955  iseqf1olemqk  10959  seqf1oglem1  10971  seqf1og  10973  seq3id3  10976  seq3id2  10978  seq3homo  10979  seqhomog  10982  expgt1  11029  m1expeven  11038  expnbnd  11116  expnlbnd2  11118  nn0ltexp2  11163  apexp1  11172  hashennn  11235  hashfibclem  11298  hashf1lem2  11302  zfz1isolem1  11308  seq3coll  11310  pfxwrdsymbg  11478  wrdind  11510  wrd2ind  11511  cjap  11688  caucvgre  11763  cvg1nlemres  11767  resqrexlemgt0  11802  resqrexlemglsq  11804  resqrexlemga  11805  resqrtcl  11811  abslt  11871  abssubap0  11873  abssubne0  11874  caubnd2  11900  qdenre  11985  maxabslemlub  11990  maxabs  11992  maxleast  11996  fimaxre2  12010  xrmaxiflemlub  12033  xrmaxif  12036  xrmaxltsup  12043  xrmaxadd  12046  xrmineqinf  12054  climuni  12078  2clim  12086  climcn1  12093  climcn2  12094  subcn2  12096  mulcn2  12097  climsqz  12120  climsqz2  12121  climcau  12132  climcvg1nlem  12134  climcaucn  12136  serf0  12137  sumrbdclem  12163  summodclem2  12168  zsumdc  12170  divcnv  12283  absltap  12295  absgtap  12296  mertenslem2  12322  ntrivcvgap  12334  prodrbdclem  12357  prodmodclem2  12363  zproddc  12365  prodssdc  12375  fprodsplitdc  12382  fprodcl2lem  12391  efcllemp  12444  tanvalap  12494  sin01bnd  12543  cos01bnd  12544  sin01gt0  12548  absef  12556  eirrap  12564  dvds0  12592  dvdsmul1  12599  dvdsmultr1d  12618  dvdslelemd  12629  divconjdvds  12635  alzdvds  12640  3dvds  12650  sqoddm1div8z  12672  nno  12692  divalglemex  12708  bits0o  12736  dvdsbnd  12752  dvdslegcd  12760  zeqzmulgcd  12766  gcd0id  12775  gcdaddm  12780  gcd1  12783  gcdabs  12784  bezoutlemnewy  12792  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlemex  12797  bezoutlemzz  12798  bezoutlemaz  12799  bezoutlembz  12800  bezoutlembi  12801  bezoutlemle  12804  bezoutlemsup  12805  mulgcd  12812  gcdzeq  12818  dvdsmulgcd  12821  sqgcd  12825  bezoutr1  12829  nninfctlemfo  12836  algcvga  12848  algfx  12849  eucalglt  12854  eucalg  12856  lcmneg  12871  lcmabs  12873  lcmgcdlem  12874  ncoprmgcdne1b  12886  mulgcddvds  12891  qredeq  12893  divgcdcoprm0  12898  cncongr1  12900  isprm2lem  12913  nprm  12920  dvdsnprmd  12922  prmdvdsfz  12937  isprm5lem  12939  coprm  12942  isprm6  12945  sqrt2irr  12960  pwbdvdslemn  12963  pwbdvdseulemle  12965  nnmaxpwlemdvds  12968  nnmaxpwlemndvds  12969  sqrt2irrap  12979  qnumdencl  12986  nn0sqdcq  13007  sqrtrirr  13008  prmdiv  13036  modprmn0modprm0  13058  prm23lt5  13065  pythagtriplem4  13070  pythagtriplem19  13084  pythagtrip  13085  pclemub  13089  pcpre1  13094  pcpremul  13095  pceulem  13096  pcqcl  13108  pcidlem  13125  pcgcd1  13130  pc2dvds  13132  dvdsprmpweqle  13139  difsqpwdvds  13140  pcadd  13142  pcmpt  13145  expnprm  13155  pockthg  13159  infpnlem2  13162  prmunb  13164  1arith  13169  4sqlem10  13189  4sqlem11  13203  4sqlem12  13204  4sqlem13m  13205  4sqlem17  13209  4sqlem18  13210  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemfrceq  13324  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemrnh  13359  ennnfonelemnn0  13365  ennnfonelemim  13367  exmidunben  13369  ctinfomlemom  13370  ctinfom  13371  ctinf  13373  omctfn  13386  nninfdclemp1  13393  setscomd  13445  imasaddfnlemg  13688  mhmf1o  13830  grpinveu  13896  grpasscan1  13921  dfgrp3mlem  13956  grp1inv  13965  issubg4m  14049  ghmf1o  14131  srgisid  14374  ringadd2  14416  ringinvnzdiv  14439  unitgrp  14507  ringelnzr  14578  lringuplu  14587  subrguss  14628  subrgintm  14635  aprcotr  14681  islmodd  14713  lssclg  14785  lss0cl  14790  lssvneln0  14794  lss1d  14804  lmodindp1  14849  rnglidlmmgm  14917  znidomb  15077  znunit  15078  znrrg  15079  rnasclassa  15122  mplsubgfilemcl  15181  mplsubgfileminv  15182  tgcl  15256  neii1  15339  neii2  15341  neiss  15342  tpnei  15352  tgrest  15361  ssrest  15374  icnpimaex  15403  lmcvg  15409  cnpnei  15411  cnptopco  15414  lmff  15441  txcnp  15463  txcn  15467  hmeontr  15505  blssec  15630  mopni3  15676  blsscls2  15685  comet  15691  bdxmet  15693  bdmopn  15696  xmettxlem  15701  xmettx  15702  addcncntoplem  15753  mpomulcn  15758  mulc1cncf  15781  cncfco  15783  cncfmptc  15788  mulcncflem  15799  mulcncf  15800  dedekindeulemlu  15813  dedekindeulemeu  15814  suplociccreex  15816  suplociccex  15817  dedekindicclemlu  15822  dedekindicclemeu  15823  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemloc  15833  ivthinc  15835  ivthreinc  15837  ivthdichlem  15843  limcimolemlt  15856  limcresi  15858  cnplimcim  15859  cnplimclemle  15860  cnplimclemr  15861  limccnpcntop  15867  limccoap  15870  dvcoapbr  15899  dvcj  15901  plyf  15929  plyaddlem1  15939  plymullem1  15940  plyco  15951  plycj  15953  plycn  15954  plyrecj  15955  dvply2g  15958  efltlemlt  15966  sin0pilem2  15975  tangtx  16031  logdivlti  16075  logdivlt  16088  rplogbval  16142  logbgcd1irraplemexp  16165  logbgcd1irraplemap  16166  logbgcd1irrap  16167  zprmlogbaplem2  16177  zprmlogbap  16179  birthdaylem1g  16186  ppiublem2  16253  chtublem  16256  chtqub  16257  perfect1  16259  perfectlem1  16260  perfectlem2  16261  bposlem6  16277  bposlem9  16280  bpos  16281  lgsval4a  16307  lgsdir2lem3  16315  lgsne0  16323  gausslemma2dlem3  16348  gausslemma2dlem4  16349  gausslemma2dlem6  16352  gausslemma2dlem7  16353  gausslemma2d  16354  lgseisenlem1  16355  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad2lem2  16367  lgsquad3  16369  2lgsoddprmlem2  16391  2sqlem8a  16407  2sqlem8  16408  2sqlem9  16409  lpvtx  16486  upgrex  16510  upgr1een  16531  edgupgren  16548  umgredg  16552  upgrpredgv  16553  upgredg2vtx  16555  upgredgpr  16556  uspgrf1oedg  16583  usgredg4  16622  uspgredgdomord  16636  usgr1vr  16655  wlkvtxiedg  16752  wlkvtxiedgg  16753  wlk1walkdom  16766  upgriswlkdc  16767  upgrwlkedg  16768  uspgr2wlkeq  16772  uspgr2wlkeqi  16774  umgrwlknloop  16775  eupth2lem2dc  16866  trlsegvdeglem1  16867  eupth2lem3lem4fi  16880  bj-exlimmpi  16964  uzdcinzz  16992  bj-charfundcALT  17001  bj-2inf  17130  bj-peano4  17147  bj-nn0suc  17156  pw1ndom3  17186  subctctexmid  17196  exmidcon  17203  nninfalllem1  17217  nninfsellemqall  17224  nninfomnilem  17227  nninffeq  17229  nnnninfex  17231  exmidsbthrlem  17233  sbthomlem  17236  refeq  17239  isomninnlem  17245  apdifflemr  17263  redcwlpo  17272  reap0  17275  nconstwlpolem  17282