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  4310  exmid1dc  4339  exmid1stab  4347  opth  4379  issod  4466  frirrg  4497  frind  4499  ralxfr2d  4612  rexxfr2d  4613  eldifpw  4625  onun2  4639  onuni  4643  elirr  4690  en2lp  4703  wetriext  4726  peano2  4744  relop  4932  elres  5101  sotri2  5188  iota4an  5361  iota5  5362  funeu  5405  funopg  5414  imadiflem  5463  funimaexglem  5467  ssimaex  5767  ffvelcdm  5844  dff3im  5856  dffo4  5859  funopsn  5894  f1eqcocnv  6000  f1oiso2  6036  riota5f  6068  riotass2  6070  acexmidlemcase  6083  elovimad  6132  ovmpodf  6223  ovmpodv2  6225  ovi3  6229  ov6g  6230  caoftrn  6339  op1steq  6417  fvdifsuppst  6488  suppssdc  6504  suppofss1dcl  6508  suppofss2dcl  6509  tfr0dm  6597  tfrlemibxssdm  6602  tfrlemi14d  6608  tfr1onlembxssdm  6618  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllembxssdm  6631  tfrcllemaccex  6636  tfrcllemres  6637  rdgivallem  6656  nnsucelsuc  6768  nnsucsssuc  6769  dcdifsnid  6781  nnawordex  6806  ersym  6823  mapvalg  6936  pmvalg  6937  mapsnd  6974  mapsn  6976  fundmen  7098  1dom1el  7111  en2  7116  pw2f1odclem  7138  mapdom1g  7151  fidceq  7175  fin0or  7194  findcard2  7197  findcard2s  7198  fidcen  7207  prfidceq  7239  fiintim  7242  suplub2ti  7347  supsnti  7351  supisoex  7355  difinfsnlem  7445  difinfsn  7446  ctm  7455  ctssdclemn0  7456  ctssdccl  7457  ctssdc  7459  enumctlemm  7460  nninfninc  7469  nnnninfeq2  7475  enomnilem  7484  exmidomniim  7487  exmidomni  7488  fodjuomnilemdc  7490  fodjuomnilemres  7494  omnimkv  7502  mkvprop  7504  omniwomnimkv  7513  en2prde  7545  pr2cv1  7547  en2eleq  7553  acfun  7569  exmidontriimlem1  7583  exmidontriimlem4  7586  exmidontriim  7587  papsym  7618  papcotr  7619  ccfunen  7636  cc4f  7641  cc4n  7643  elni2  7687  mulclpi  7701  nlt1pig  7714  indpi  7715  recclnq  7765  ltexnqq  7781  halfnqq  7783  prarloclemarch  7791  prarloclemarch2  7792  prop  7848  prltlu  7860  prarloclem3step  7869  prarloclem5  7873  prarloclem  7874  prarloc  7876  prarloc2  7877  genpml  7890  genpmu  7891  genprndl  7894  genprndu  7895  genpdisj  7896  addnqprllem  7900  addnqprulem  7901  addlocprlemeq  7906  addlocprlemgt  7907  addlocprlem  7908  addlocpr  7909  nqprloc  7918  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  appdivnq  7936  prmuloc  7939  prmuloc2  7940  mullocprlem  7943  mullocpr  7944  mulnqprlemrl  7946  mulnqprlemru  7947  ltprordil  7962  ltpopr  7968  ltsopr  7969  ltaddpr  7970  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  ltexprlemloc  7980  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  ltaprg  7992  recexprlemm  7997  recexprlem1ssl  8006  recexprlem1ssu  8007  aptiprleml  8012  aptiprlemu  8013  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlem1  8032  archrecpr  8037  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlem1  8052  caucvgprlemlim  8054  caucvgprprlemnbj  8066  caucvgprprlemml  8067  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemopu  8072  caucvgprprlemupu  8073  caucvgprprlemdisj  8075  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  caucvgprprlemaddq  8081  caucvgprprlemlim  8084  suplocexprlemss  8088  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  suplocexprlemlub  8097  recexgt0sr  8146  mulgt0sr  8151  archsr  8155  caucvgsrlemoffcau  8171  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  cnm  8205  axarch  8264  axcaucvglemcau  8271  axpre-suploclemres  8274  lelttr  8420  ltletr  8421  ltled  8452  cnegexlem1  8508  cnegexlem2  8509  renegcl  8594  negf1o  8716  gt0add  8909  apreap  8923  apirr  8941  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  mulap0r  8951  apti  8958  aprcl  8982  aptap  8986  recexap  8989  mulap0  8990  receuap  9007  mul0eqap  9008  lep1  9183  lem1  9185  letrp1  9186  recreclt  9238  lbinf  9286  suprubex  9289  nnrecgt0  9351  bndndx  9573  nn0ge2m1nn  9638  elnn0z  9668  peano2z  9691  zaddcl  9695  ztri3or0  9697  zltnle  9701  zdceq  9731  zdcle  9732  zdclt  9733  zdiv  9745  zeo  9762  fnn0ind  9773  btwnz  9776  uzm1  9969  uzp1  9972  indstr  10009  supinfneg  10011  infsupneg  10012  eluzdc  10026  nn01to3  10033  qapne  10055  xrltled  10218  xrlelttr  10225  xrltletr  10226  ge0nemnf  10243  fzdcel  10461  elfzouz2  10586  fzoss1  10597  fzospliti  10602  elincfzoext  10628  fzocatel  10634  fzostep1  10673  zsupcllemstep  10679  zsupcl  10681  infssuzledc  10684  qtri3or  10692  qltnle  10695  qdceq  10696  qdclt  10697  exbtwnzlemex  10701  rebtwn2zlemstep  10704  rebtwn2z  10706  qbtwnxr  10709  ioom  10712  ico0  10713  ioc0  10714  flqeqceilz  10776  modqadd1  10819  modqmul1  10835  frec2uzuzd  10860  frec2uzlt2d  10862  frec2uzf1od  10864  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgdomlem  10875  uzsinds  10902  seqvalcd  10919  seqovcd  10925  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  monoord  10943  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  iseqf1olemab  10960  iseqf1olemnanb  10961  iseqf1olemqk  10965  seqf1oglem1  10977  seqf1og  10979  seq3id3  10982  seq3id2  10984  seq3homo  10985  seqhomog  10988  expgt1  11035  m1expeven  11044  expnbnd  11122  expnlbnd2  11124  nn0ltexp2  11169  apexp1  11178  hashennn  11241  hashfibclem  11304  hashf1lem2  11308  zfz1isolem1  11314  seq3coll  11316  pfxwrdsymbg  11484  wrdind  11516  wrd2ind  11517  cjap  11694  caucvgre  11769  cvg1nlemres  11773  resqrexlemgt0  11808  resqrexlemglsq  11810  resqrexlemga  11811  resqrtcl  11817  abslt  11877  abssubap0  11879  abssubne0  11880  caubnd2  11906  qdenre  11991  maxabslemlub  11996  maxabs  11998  maxleast  12002  fimaxre2  12016  xrmaxiflemlub  12039  xrmaxif  12042  xrmaxltsup  12049  xrmaxadd  12052  xrmineqinf  12060  climuni  12084  2clim  12092  climcn1  12099  climcn2  12100  subcn2  12102  mulcn2  12103  climsqz  12126  climsqz2  12127  climcau  12138  climcvg1nlem  12140  climcaucn  12142  serf0  12143  sumrbdclem  12169  summodclem2  12174  zsumdc  12176  divcnv  12289  absltap  12301  absgtap  12302  mertenslem2  12328  ntrivcvgap  12340  prodrbdclem  12363  prodmodclem2  12369  zproddc  12371  prodssdc  12381  fprodsplitdc  12388  fprodcl2lem  12397  efcllemp  12450  tanvalap  12500  sin01bnd  12549  cos01bnd  12550  sin01gt0  12554  absef  12562  eirrap  12570  dvds0  12598  dvdsmul1  12605  dvdsmultr1d  12624  dvdslelemd  12635  divconjdvds  12641  alzdvds  12646  3dvds  12656  sqoddm1div8z  12678  nno  12698  divalglemex  12714  bits0o  12742  dvdsbnd  12758  dvdslegcd  12766  zeqzmulgcd  12772  gcd0id  12781  gcdaddm  12786  gcd1  12789  gcdabs  12790  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemex  12803  bezoutlemzz  12804  bezoutlemaz  12805  bezoutlembz  12806  bezoutlembi  12807  bezoutlemle  12810  bezoutlemsup  12811  mulgcd  12818  gcdzeq  12824  dvdsmulgcd  12827  sqgcd  12831  bezoutr1  12835  nninfctlemfo  12842  algcvga  12854  algfx  12855  eucalglt  12860  eucalg  12862  lcmneg  12877  lcmabs  12879  lcmgcdlem  12880  ncoprmgcdne1b  12892  mulgcddvds  12897  qredeq  12899  divgcdcoprm0  12904  cncongr1  12906  isprm2lem  12919  nprm  12926  dvdsnprmd  12928  prmdvdsfz  12943  isprm5lem  12945  coprm  12948  isprm6  12951  sqrt2irr  12966  pwbdvdslemn  12969  pwbdvdseulemle  12971  nnmaxpwlemdvds  12974  nnmaxpwlemndvds  12975  sqrt2irrap  12985  qnumdencl  12992  nn0sqdcq  13013  sqrtrirr  13014  prmdiv  13042  modprmn0modprm0  13064  prm23lt5  13071  pythagtriplem4  13076  pythagtriplem19  13090  pythagtrip  13091  pclemub  13095  pcpre1  13100  pcpremul  13101  pceulem  13102  pcqcl  13114  pcidlem  13131  pcgcd1  13136  pc2dvds  13138  dvdsprmpweqle  13145  difsqpwdvds  13146  pcadd  13148  pcmpt  13151  expnprm  13161  pockthg  13165  infpnlem2  13168  prmunb  13170  1arith  13175  4sqlem10  13195  4sqlem11  13209  4sqlem12  13210  4sqlem13m  13211  4sqlem17  13215  4sqlem18  13216  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfrceq  13330  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemrnh  13365  ennnfonelemnn0  13371  ennnfonelemim  13373  exmidunben  13375  ctinfomlemom  13376  ctinfom  13377  ctinf  13379  omctfn  13392  nninfdclemp1  13399  setscomd  13451  imasaddfnlemg  13694  mhmf1o  13836  grpinveu  13902  grpasscan1  13927  dfgrp3mlem  13962  grp1inv  13971  issubg4m  14055  ghmf1o  14137  gsum2d2fi  14274  srgisid  14397  ringadd2  14439  ringinvnzdiv  14462  unitgrp  14532  ringelnzr  14603  lringuplu  14612  subrguss  14653  subrgintm  14660  aprcotr  14706  islmodd  14738  lssclg  14810  lss0cl  14815  lssvneln0  14819  lss1d  14829  lmodindp1  14874  rnglidlmmgm  14942  znidomb  15102  znunit  15103  znrrg  15104  rnasclassa  15147  mplsubgfilemcl  15215  mplsubgfileminv  15216  tgcl  15290  neii1  15373  neii2  15375  neiss  15376  tpnei  15386  tgrest  15395  ssrest  15408  icnpimaex  15437  lmcvg  15443  cnpnei  15445  cnptopco  15448  lmff  15475  txcnp  15497  txcn  15501  hmeontr  15539  blssec  15664  mopni3  15710  blsscls2  15719  comet  15725  bdxmet  15727  bdmopn  15730  xmettxlem  15735  xmettx  15736  addcncntoplem  15787  mpomulcn  15792  mulc1cncf  15815  cncfco  15817  cncfmptc  15822  mulcncflem  15833  mulcncf  15834  dedekindeulemlu  15847  dedekindeulemeu  15848  suplociccreex  15850  suplociccex  15851  dedekindicclemlu  15856  dedekindicclemeu  15857  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemloc  15867  ivthinc  15869  ivthreinc  15871  ivthdichlem  15877  limcimolemlt  15890  limcresi  15892  cnplimcim  15893  cnplimclemle  15894  cnplimclemr  15895  limccnpcntop  15901  limccoap  15904  dvcoapbr  15933  dvcj  15935  plyf  15963  plyaddlem1  15973  plymullem1  15974  plyco  15985  plycj  15987  plycn  15988  plyrecj  15989  dvply2g  15992  efltlemlt  16000  sin0pilem2  16009  tangtx  16065  logdivlti  16111  logdivlt  16124  rplogbval  16181  logbgcd1irraplemexp  16204  logbgcd1irraplemap  16205  logbgcd1irrap  16206  zprmlogbaplem2  16216  zprmlogbap  16218  birthdaylem1g  16225  ppiublem2  16292  chtublem  16295  chtqub  16296  perfect1  16298  perfectlem1  16299  perfectlem2  16300  bposlem6  16316  bposlem9  16319  bpos  16320  lgsval4a  16346  lgsdir2lem3  16354  lgsne0  16362  gausslemma2dlem3  16387  gausslemma2dlem4  16388  gausslemma2dlem6  16391  gausslemma2dlem7  16392  gausslemma2d  16393  lgseisenlem1  16394  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2lem2  16406  lgsquad3  16408  2lgsoddprmlem2  16430  2sqlem8a  16446  2sqlem8  16447  2sqlem9  16448  lpvtx  16525  upgrex  16549  upgr1een  16570  edgupgren  16587  umgredg  16591  upgrpredgv  16592  upgredg2vtx  16594  upgredgpr  16595  uspgrf1oedg  16622  usgredg4  16661  uspgredgdomord  16675  usgr1vr  16694  wlkvtxiedg  16791  wlkvtxiedgg  16792  wlk1walkdom  16805  upgriswlkdc  16806  upgrwlkedg  16807  uspgr2wlkeq  16811  uspgr2wlkeqi  16813  umgrwlknloop  16814  eupth2lem2dc  16905  trlsegvdeglem1  16906  eupth2lem3lem4fi  16919  bj-exlimmpi  17003  uzdcinzz  17031  bj-charfundcALT  17040  bj-2inf  17169  bj-peano4  17186  bj-nn0suc  17195  pw1ndom3  17225  subctctexmid  17235  exmidcon  17242  nninfalllem1  17257  nninfsellemqall  17264  nninfomnilem  17267  nninffeq  17269  nnnninfex  17271  exmidsbthrlem  17273  sbthomlem  17276  refeq  17279  isomninnlem  17285  apdifflemr  17303  redcwlpo  17312  reap0  17315  nconstwlpolem  17322