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  621  mt2d  626  mpjaod  719  stdcndcOLD  847  impidc  859  jadc  864  pm2.54dc  892  oplem1  977  mp3and  1351  xor3dc  1398  exlimdd  1886  exlimddv  1913  eqrdav  2195  necon1aidc  2418  necon1bidc  2419  necon4aidc  2435  reximddv  2600  reximssdv  2601  rexlimddv  2619  vtoclgft  2814  rspcedvd  2874  sseldd  3184  ssneldd  3186  tpid3g  3737  preq12b  3800  axpweq  4204  exmid1dc  4233  exmid1stab  4241  opth  4270  issod  4354  frirrg  4385  frind  4387  ralxfr2d  4499  rexxfr2d  4500  eldifpw  4512  onun2  4526  onuni  4530  elirr  4577  en2lp  4590  wetriext  4613  peano2  4631  relop  4816  elres  4982  sotri2  5067  iota4an  5239  iota5  5240  funeu  5283  funopg  5292  imadiflem  5337  funimaexglem  5341  ssimaex  5622  ffvelcdm  5695  dff3im  5707  dffo4  5710  f1eqcocnv  5838  f1oiso2  5874  riota5f  5902  riotass2  5904  acexmidlemcase  5917  ovmpodf  6054  ovmpodv2  6056  ovi3  6060  ov6g  6061  caoftrn  6163  op1steq  6237  tfr0dm  6380  tfrlemibxssdm  6385  tfrlemi14d  6391  tfr1onlembxssdm  6401  tfr1onlemaccex  6406  tfr1onlemres  6407  tfrcllembxssdm  6414  tfrcllemaccex  6419  tfrcllemres  6420  rdgivallem  6439  nnsucelsuc  6549  nnsucsssuc  6550  dcdifsnid  6562  nnawordex  6587  ersym  6604  mapvalg  6717  pmvalg  6718  mapsn  6749  fundmen  6865  pw2f1odclem  6895  mapdom1g  6908  fidceq  6930  fin0or  6947  findcard2  6950  findcard2s  6951  prfidceq  6989  fiintim  6992  suplub2ti  7067  supsnti  7071  supisoex  7075  difinfsnlem  7165  difinfsn  7166  ctm  7175  ctssdclemn0  7176  ctssdccl  7177  ctssdc  7179  enumctlemm  7180  nninfninc  7189  nnnninfeq2  7195  enomnilem  7204  exmidomniim  7207  exmidomni  7208  fodjuomnilemdc  7210  fodjuomnilemres  7214  omnimkv  7222  mkvprop  7224  omniwomnimkv  7233  en2eleq  7262  acfun  7274  exmidontriimlem1  7288  exmidontriimlem4  7291  exmidontriim  7292  ccfunen  7331  cc4f  7336  cc4n  7338  elni2  7381  mulclpi  7395  nlt1pig  7408  indpi  7409  recclnq  7459  ltexnqq  7475  halfnqq  7477  prarloclemarch  7485  prarloclemarch2  7486  prop  7542  prltlu  7554  prarloclem3step  7563  prarloclem5  7567  prarloclem  7568  prarloc  7570  prarloc2  7571  genpml  7584  genpmu  7585  genprndl  7588  genprndu  7589  genpdisj  7590  addnqprllem  7594  addnqprulem  7595  addlocprlemeq  7600  addlocprlemgt  7601  addlocprlem  7602  addlocpr  7603  nqprloc  7612  nqprl  7618  nqpru  7619  addnqprlemrl  7624  addnqprlemru  7625  appdivnq  7630  prmuloc  7633  prmuloc2  7634  mullocprlem  7637  mullocpr  7638  mulnqprlemrl  7640  mulnqprlemru  7641  ltprordil  7656  ltpopr  7662  ltsopr  7663  ltaddpr  7664  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemlol  7669  ltexprlemopu  7670  ltexprlemupu  7671  ltexprlemloc  7674  ltexprlemfl  7676  ltexprlemrl  7677  ltexprlemfu  7678  ltexprlemru  7679  ltaprg  7686  recexprlemm  7691  recexprlem1ssl  7700  recexprlem1ssu  7701  aptiprleml  7706  aptiprlemu  7707  archpr  7710  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemopu  7715  cauappcvgprlemupu  7716  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  cauappcvgprlem1  7726  archrecpr  7731  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemopu  7738  caucvgprlemupu  7739  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemladdfu  7744  caucvgprlem1  7746  caucvgprlemlim  7748  caucvgprprlemnbj  7760  caucvgprprlemml  7761  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemupu  7767  caucvgprprlemdisj  7769  caucvgprprlemloc  7770  caucvgprprlemexbt  7773  caucvgprprlemaddq  7775  caucvgprprlemlim  7778  suplocexprlemss  7782  suplocexprlemrl  7784  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  suplocexprlemlub  7791  recexgt0sr  7840  mulgt0sr  7845  archsr  7849  caucvgsrlemoffcau  7865  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  cnm  7899  axarch  7958  axcaucvglemcau  7965  axpre-suploclemres  7968  lelttr  8115  ltletr  8116  ltled  8145  cnegexlem1  8201  cnegexlem2  8202  renegcl  8287  negf1o  8408  gt0add  8600  apreap  8614  apirr  8632  apsym  8633  apcotr  8634  apadd1  8635  apneg  8638  mulext1  8639  mulap0r  8642  apti  8649  aprcl  8673  aptap  8677  recexap  8680  mulap0  8681  receuap  8696  mul0eqap  8697  lep1  8872  lem1  8874  letrp1  8875  recreclt  8927  lbinf  8975  suprubex  8978  nnrecgt0  9028  bndndx  9248  nn0ge2m1nn  9309  elnn0z  9339  peano2z  9362  zaddcl  9366  ztri3or0  9368  zltnle  9372  zdceq  9401  zdcle  9402  zdclt  9403  zdiv  9414  zeo  9431  fnn0ind  9442  btwnz  9445  uzm1  9632  uzp1  9635  indstr  9667  supinfneg  9669  infsupneg  9670  eluzdc  9684  nn01to3  9691  qapne  9713  xrltled  9874  xrlelttr  9881  xrltletr  9882  ge0nemnf  9899  fzdcel  10115  elfzouz2  10237  fzoss1  10247  fzospliti  10252  fzocatel  10275  fzostep1  10313  zsupcllemstep  10319  zsupcl  10321  infssuzledc  10324  qtri3or  10330  qltnle  10333  qdceq  10334  qdclt  10335  exbtwnzlemex  10339  rebtwn2zlemstep  10342  rebtwn2z  10344  qbtwnxr  10347  ioom  10350  ico0  10351  ioc0  10352  flqeqceilz  10410  modqadd1  10453  modqmul1  10469  frec2uzuzd  10494  frec2uzlt2d  10496  frec2uzf1od  10498  frecuzrdgrrn  10500  frec2uzrdg  10501  frecuzrdgrcl  10502  frecuzrdgsuc  10506  frecuzrdgrclt  10507  frecuzrdgdomlem  10509  uzsinds  10536  seqvalcd  10553  seqovcd  10559  seq3fveq2  10567  seqfveq2g  10569  seq3shft2  10573  seqshft2g  10574  monoord  10577  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  iseqf1olemab  10594  iseqf1olemnanb  10595  iseqf1olemqk  10599  seqf1oglem1  10611  seqf1og  10613  seq3id3  10616  seq3id2  10618  seq3homo  10619  seqhomog  10622  expgt1  10669  m1expeven  10678  expnbnd  10755  expnlbnd2  10757  nn0ltexp2  10801  apexp1  10810  hashennn  10872  zfz1isolem1  10932  seq3coll  10934  cjap  11071  caucvgre  11146  cvg1nlemres  11150  resqrexlemgt0  11185  resqrexlemglsq  11187  resqrexlemga  11188  resqrtcl  11194  abslt  11253  abssubap0  11255  abssubne0  11256  caubnd2  11282  qdenre  11367  maxabslemlub  11372  maxabs  11374  maxleast  11378  fimaxre2  11392  xrmaxiflemlub  11413  xrmaxif  11416  xrmaxltsup  11423  xrmaxadd  11426  xrmineqinf  11434  climuni  11458  2clim  11466  climcn1  11473  climcn2  11474  subcn2  11476  mulcn2  11477  climsqz  11500  climsqz2  11501  climcau  11512  climcvg1nlem  11514  climcaucn  11516  serf0  11517  sumrbdclem  11542  summodclem2  11547  zsumdc  11549  divcnv  11662  absltap  11674  absgtap  11675  mertenslem2  11701  ntrivcvgap  11713  prodrbdclem  11736  prodmodclem2  11742  zproddc  11744  prodssdc  11754  fprodsplitdc  11761  fprodcl2lem  11770  efcllemp  11823  tanvalap  11873  sin01bnd  11922  cos01bnd  11923  sin01gt0  11927  absef  11935  eirrap  11943  dvds0  11971  dvdsmul1  11978  dvdsmultr1d  11997  dvdslelemd  12008  divconjdvds  12014  alzdvds  12019  3dvds  12029  sqoddm1div8z  12051  nno  12071  divalglemex  12087  bits0o  12114  dvdsbnd  12123  dvdslegcd  12131  zeqzmulgcd  12137  gcd0id  12146  gcdaddm  12151  gcd1  12154  gcdabs  12155  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlemex  12168  bezoutlemzz  12169  bezoutlemaz  12170  bezoutlembz  12171  bezoutlembi  12172  bezoutlemle  12175  bezoutlemsup  12176  mulgcd  12183  gcdzeq  12189  dvdsmulgcd  12192  sqgcd  12196  bezoutr1  12200  nninfctlemfo  12207  algcvga  12219  algfx  12220  eucalglt  12225  eucalg  12227  lcmneg  12242  lcmabs  12244  lcmgcdlem  12245  ncoprmgcdne1b  12257  mulgcddvds  12262  qredeq  12264  divgcdcoprm0  12269  cncongr1  12271  isprm2lem  12284  nprm  12291  dvdsnprmd  12293  prmdvdsfz  12307  isprm5lem  12309  coprm  12312  isprm6  12315  sqrt2irr  12330  pw2dvdslemn  12333  pw2dvdseulemle  12335  oddpwdclemdvds  12338  oddpwdclemndvds  12339  sqrt2irrap  12348  qnumdencl  12355  prmdiv  12403  modprmn0modprm0  12425  prm23lt5  12432  pythagtriplem4  12437  pythagtriplem19  12451  pythagtrip  12452  pclemub  12456  pcpre1  12461  pcpremul  12462  pceulem  12463  pcqcl  12475  pcidlem  12492  pcgcd1  12497  pc2dvds  12499  dvdsprmpweqle  12506  difsqpwdvds  12507  pcadd  12509  pcmpt  12512  expnprm  12522  pockthg  12526  infpnlem2  12529  prmunb  12531  1arith  12536  4sqlem10  12556  4sqlem11  12570  4sqlem12  12571  4sqlem13m  12572  4sqlem17  12576  4sqlem18  12577  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemrnh  12633  ennnfonelemnn0  12639  ennnfonelemim  12641  exmidunben  12643  ctinfomlemom  12644  ctinfom  12645  ctinf  12647  omctfn  12660  nninfdclemp1  12667  setscomd  12719  imasaddfnlemg  12957  mhmf1o  13102  grpinveu  13170  grpasscan1  13195  dfgrp3mlem  13230  grp1inv  13239  issubg4m  13323  ghmf1o  13405  srgisid  13542  ringadd2  13583  ringinvnzdiv  13606  unitgrp  13672  ringelnzr  13743  lringuplu  13752  subrguss  13792  subrgintm  13799  aprcotr  13841  islmodd  13849  lssclg  13920  lss0cl  13925  lssvneln0  13929  lss1d  13939  lmodindp1  13984  rnglidlmmgm  14052  znidomb  14214  znunit  14215  znrrg  14216  tgcl  14300  neii1  14383  neii2  14385  neiss  14386  tpnei  14396  tgrest  14405  ssrest  14418  icnpimaex  14447  lmcvg  14453  cnpnei  14455  cnptopco  14458  lmff  14485  txcnp  14507  txcn  14511  hmeontr  14549  blssec  14674  mopni3  14720  blsscls2  14729  comet  14735  bdxmet  14737  bdmopn  14740  xmettxlem  14745  xmettx  14746  addcncntoplem  14797  mpomulcn  14802  mulc1cncf  14825  cncfco  14827  cncfmptc  14832  mulcncflem  14843  mulcncf  14844  dedekindeulemlu  14857  dedekindeulemeu  14858  suplociccreex  14860  suplociccex  14861  dedekindicclemlu  14866  dedekindicclemeu  14867  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemloc  14877  ivthinc  14879  ivthreinc  14881  ivthdichlem  14887  limcimolemlt  14900  limcresi  14902  cnplimcim  14903  cnplimclemle  14904  cnplimclemr  14905  limccnpcntop  14911  limccoap  14914  dvcoapbr  14943  dvcj  14945  plyf  14973  plyaddlem1  14983  plymullem1  14984  plyco  14995  plycj  14997  plycn  14998  plyrecj  14999  dvply2g  15002  efltlemlt  15010  sin0pilem2  15018  tangtx  15074  logdivlti  15117  rplogbval  15181  logbgcd1irraplemexp  15204  logbgcd1irraplemap  15205  logbgcd1irrap  15206  perfect1  15234  perfectlem1  15235  perfectlem2  15236  lgsval4a  15263  lgsdir2lem3  15271  lgsne0  15279  gausslemma2dlem3  15304  gausslemma2dlem4  15305  gausslemma2dlem6  15308  gausslemma2dlem7  15309  gausslemma2d  15310  lgseisenlem1  15311  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem2  15323  lgsquad3  15325  2lgsoddprmlem2  15347  2sqlem8a  15363  2sqlem8  15364  2sqlem9  15365  bj-exlimmpi  15416  uzdcinzz  15444  bj-charfundcALT  15455  bj-2inf  15584  bj-peano4  15601  bj-nn0suc  15610  1dom1el  15637  subctctexmid  15645  nninfalllem1  15652  nninfsellemqall  15659  nninfomnilem  15662  nninffeq  15664  exmidsbthrlem  15666  sbthomlem  15669  refeq  15672  isomninnlem  15674  apdifflemr  15691  redcwlpo  15699  reap0  15702  nconstwlpolem  15709