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  700  mpjaod  726  stdcndcOLD  854  impidc  866  jadc  871  pm2.54dc  899  oplem1  984  mp3and  1377  xor3dc  1432  exlimdd  1921  exlimddv  1950  eqrdav  2233  necon1aidc  2465  necon1bidc  2466  necon4aidc  2482  reximddv  2647  reximssdv  2648  rexlimddv  2667  vtoclgft  2867  rspcedvd  2929  sseldd  3243  ssneldd  3245  tpid3g  3812  preq12b  3879  axpweq  4289  exmid1dc  4318  exmid1stab  4326  opth  4358  issod  4445  frirrg  4476  frind  4478  ralxfr2d  4590  rexxfr2d  4591  eldifpw  4603  onun2  4617  onuni  4621  elirr  4668  en2lp  4681  wetriext  4704  peano2  4722  relop  4910  elres  5079  sotri2  5165  iota4an  5338  iota5  5339  funeu  5382  funopg  5391  imadiflem  5440  funimaexglem  5444  ssimaex  5743  ffvelcdm  5815  dff3im  5827  dffo4  5830  funopsn  5865  f1eqcocnv  5970  f1oiso2  6006  riota5f  6038  riotass2  6040  acexmidlemcase  6053  elovimad  6102  ovmpodf  6193  ovmpodv2  6195  ovi3  6199  ov6g  6200  caoftrn  6308  op1steq  6386  fvdifsuppst  6457  suppssdc  6473  suppofss1dcl  6477  suppofss2dcl  6478  tfr0dm  6566  tfrlemibxssdm  6571  tfrlemi14d  6577  tfr1onlembxssdm  6587  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllembxssdm  6600  tfrcllemaccex  6605  tfrcllemres  6606  rdgivallem  6625  nnsucelsuc  6737  nnsucsssuc  6738  dcdifsnid  6750  nnawordex  6775  ersym  6792  mapvalg  6905  pmvalg  6906  mapsnd  6936  mapsn  6938  fundmen  7060  1dom1el  7073  en2  7078  pw2f1odclem  7100  mapdom1g  7113  fidceq  7137  fin0or  7156  findcard2  7159  findcard2s  7160  fidcen  7169  prfidceq  7201  fiintim  7204  suplub2ti  7305  supsnti  7309  supisoex  7313  difinfsnlem  7403  difinfsn  7404  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  nninfninc  7427  nnnninfeq2  7433  enomnilem  7442  exmidomniim  7445  exmidomni  7446  fodjuomnilemdc  7448  fodjuomnilemres  7452  omnimkv  7460  mkvprop  7462  omniwomnimkv  7471  en2prde  7503  pr2cv1  7505  en2eleq  7511  acfun  7527  exmidontriimlem1  7541  exmidontriimlem4  7544  exmidontriim  7545  papsym  7576  papcotr  7577  ccfunen  7594  cc4f  7599  cc4n  7601  elni2  7645  mulclpi  7659  nlt1pig  7672  indpi  7673  recclnq  7723  ltexnqq  7739  halfnqq  7741  prarloclemarch  7749  prarloclemarch2  7750  prop  7806  prltlu  7818  prarloclem3step  7827  prarloclem5  7831  prarloclem  7832  prarloc  7834  prarloc2  7835  genpml  7848  genpmu  7849  genprndl  7852  genprndu  7853  genpdisj  7854  addnqprllem  7858  addnqprulem  7859  addlocprlemeq  7864  addlocprlemgt  7865  addlocprlem  7866  addlocpr  7867  nqprloc  7876  nqprl  7882  nqpru  7883  addnqprlemrl  7888  addnqprlemru  7889  appdivnq  7894  prmuloc  7897  prmuloc2  7898  mullocprlem  7901  mullocpr  7902  mulnqprlemrl  7904  mulnqprlemru  7905  ltprordil  7920  ltpopr  7926  ltsopr  7927  ltaddpr  7928  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemloc  7938  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  ltaprg  7950  recexprlemm  7955  recexprlem1ssl  7964  recexprlem1ssu  7965  aptiprleml  7970  aptiprlemu  7971  archpr  7974  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlem1  7990  archrecpr  7995  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlem1  8010  caucvgprlemlim  8012  caucvgprprlemnbj  8024  caucvgprprlemml  8025  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemupu  8031  caucvgprprlemdisj  8033  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  caucvgprprlemlim  8042  suplocexprlemss  8046  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  recexgt0sr  8104  mulgt0sr  8109  archsr  8113  caucvgsrlemoffcau  8129  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  cnm  8163  axarch  8222  axcaucvglemcau  8229  axpre-suploclemres  8232  lelttr  8378  ltletr  8379  ltled  8408  cnegexlem1  8464  cnegexlem2  8465  renegcl  8550  negf1o  8672  gt0add  8864  apreap  8878  apirr  8896  apsym  8897  apcotr  8898  apadd1  8899  apneg  8902  mulext1  8903  mulap0r  8906  apti  8913  aprcl  8937  aptap  8941  recexap  8944  mulap0  8945  receuap  8960  mul0eqap  8961  lep1  9136  lem1  9138  letrp1  9139  recreclt  9191  lbinf  9239  suprubex  9242  nnrecgt0  9292  bndndx  9512  nn0ge2m1nn  9577  elnn0z  9607  peano2z  9630  zaddcl  9634  ztri3or0  9636  zltnle  9640  zdceq  9670  zdcle  9671  zdclt  9672  zdiv  9684  zeo  9701  fnn0ind  9712  btwnz  9715  uzm1  9903  uzp1  9906  indstr  9943  supinfneg  9945  infsupneg  9946  eluzdc  9960  nn01to3  9967  qapne  9989  xrltled  10151  xrlelttr  10158  xrltletr  10159  ge0nemnf  10176  fzdcel  10394  elfzouz2  10518  fzoss1  10529  fzospliti  10534  elincfzoext  10560  fzocatel  10566  fzostep1  10605  zsupcllemstep  10611  zsupcl  10613  infssuzledc  10616  qtri3or  10624  qltnle  10627  qdceq  10628  qdclt  10629  exbtwnzlemex  10633  rebtwn2zlemstep  10636  rebtwn2z  10638  qbtwnxr  10641  ioom  10644  ico0  10645  ioc0  10646  flqeqceilz  10704  modqadd1  10747  modqmul1  10763  frec2uzuzd  10788  frec2uzlt2d  10790  frec2uzf1od  10792  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgdomlem  10803  uzsinds  10830  seqvalcd  10847  seqovcd  10853  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord  10871  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  iseqf1olemab  10888  iseqf1olemnanb  10889  iseqf1olemqk  10893  seqf1oglem1  10905  seqf1og  10907  seq3id3  10910  seq3id2  10912  seq3homo  10913  seqhomog  10916  expgt1  10963  m1expeven  10972  expnbnd  11050  expnlbnd2  11052  nn0ltexp2  11096  apexp1  11105  hashennn  11168  hashfibclem  11231  zfz1isolem1  11237  seq3coll  11239  pfxwrdsymbg  11407  wrdind  11439  wrd2ind  11440  cjap  11616  caucvgre  11691  cvg1nlemres  11695  resqrexlemgt0  11730  resqrexlemglsq  11732  resqrexlemga  11733  resqrtcl  11739  abslt  11798  abssubap0  11800  abssubne0  11801  caubnd2  11827  qdenre  11912  maxabslemlub  11917  maxabs  11919  maxleast  11923  fimaxre2  11937  xrmaxiflemlub  11958  xrmaxif  11961  xrmaxltsup  11968  xrmaxadd  11971  xrmineqinf  11979  climuni  12003  2clim  12011  climcn1  12018  climcn2  12019  subcn2  12021  mulcn2  12022  climsqz  12045  climsqz2  12046  climcau  12057  climcvg1nlem  12059  climcaucn  12061  serf0  12062  sumrbdclem  12088  summodclem2  12093  zsumdc  12095  divcnv  12208  absltap  12220  absgtap  12221  mertenslem2  12247  ntrivcvgap  12259  prodrbdclem  12282  prodmodclem2  12288  zproddc  12290  prodssdc  12300  fprodsplitdc  12307  fprodcl2lem  12316  efcllemp  12369  tanvalap  12419  sin01bnd  12468  cos01bnd  12469  sin01gt0  12473  absef  12481  eirrap  12489  dvds0  12517  dvdsmul1  12524  dvdsmultr1d  12543  dvdslelemd  12554  divconjdvds  12560  alzdvds  12565  3dvds  12575  sqoddm1div8z  12597  nno  12617  divalglemex  12633  bits0o  12661  dvdsbnd  12677  dvdslegcd  12685  zeqzmulgcd  12691  gcd0id  12700  gcdaddm  12705  gcd1  12708  gcdabs  12709  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlemex  12722  bezoutlemzz  12723  bezoutlemaz  12724  bezoutlembz  12725  bezoutlembi  12726  bezoutlemle  12729  bezoutlemsup  12730  mulgcd  12737  gcdzeq  12743  dvdsmulgcd  12746  sqgcd  12750  bezoutr1  12754  nninfctlemfo  12761  algcvga  12773  algfx  12774  eucalglt  12779  eucalg  12781  lcmneg  12796  lcmabs  12798  lcmgcdlem  12799  ncoprmgcdne1b  12811  mulgcddvds  12816  qredeq  12818  divgcdcoprm0  12823  cncongr1  12825  isprm2lem  12838  nprm  12845  dvdsnprmd  12847  prmdvdsfz  12861  isprm5lem  12863  coprm  12866  isprm6  12869  sqrt2irr  12884  pw2dvdslemn  12887  pw2dvdseulemle  12889  oddpwdclemdvds  12892  oddpwdclemndvds  12893  sqrt2irrap  12902  qnumdencl  12909  prmdiv  12957  modprmn0modprm0  12979  prm23lt5  12986  pythagtriplem4  12991  pythagtriplem19  13005  pythagtrip  13006  pclemub  13010  pcpre1  13015  pcpremul  13016  pceulem  13017  pcqcl  13029  pcidlem  13046  pcgcd1  13051  pc2dvds  13053  dvdsprmpweqle  13060  difsqpwdvds  13061  pcadd  13063  pcmpt  13066  expnprm  13076  pockthg  13080  infpnlem2  13083  prmunb  13085  1arith  13090  4sqlem10  13110  4sqlem11  13124  4sqlem12  13125  4sqlem13m  13126  4sqlem17  13130  4sqlem18  13131  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfrceq  13216  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemrnh  13251  ennnfonelemnn0  13257  ennnfonelemim  13259  exmidunben  13261  ctinfomlemom  13262  ctinfom  13263  ctinf  13265  omctfn  13278  nninfdclemp1  13285  setscomd  13337  imasaddfnlemg  13578  mhmf1o  13725  grpinveu  13793  grpasscan1  13818  dfgrp3mlem  13853  grp1inv  13862  issubg4m  13946  ghmf1o  14028  srgisid  14229  ringadd2  14270  ringinvnzdiv  14293  unitgrp  14361  ringelnzr  14432  lringuplu  14441  subrguss  14482  subrgintm  14489  aprcotr  14535  islmodd  14567  lssclg  14638  lss0cl  14643  lssvneln0  14647  lss1d  14657  lmodindp1  14702  rnglidlmmgm  14770  znidomb  14932  znunit  14933  znrrg  14934  mplsubgfilemcl  14980  mplsubgfileminv  14981  tgcl  15055  neii1  15138  neii2  15140  neiss  15141  tpnei  15151  tgrest  15160  ssrest  15173  icnpimaex  15202  lmcvg  15208  cnpnei  15210  cnptopco  15213  lmff  15240  txcnp  15262  txcn  15266  hmeontr  15304  blssec  15429  mopni3  15475  blsscls2  15484  comet  15490  bdxmet  15492  bdmopn  15495  xmettxlem  15500  xmettx  15501  addcncntoplem  15552  mpomulcn  15557  mulc1cncf  15580  cncfco  15582  cncfmptc  15587  mulcncflem  15598  mulcncf  15599  dedekindeulemlu  15612  dedekindeulemeu  15613  suplociccreex  15615  suplociccex  15616  dedekindicclemlu  15621  dedekindicclemeu  15622  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemloc  15632  ivthinc  15634  ivthreinc  15636  ivthdichlem  15642  limcimolemlt  15655  limcresi  15657  cnplimcim  15658  cnplimclemle  15659  cnplimclemr  15660  limccnpcntop  15666  limccoap  15669  dvcoapbr  15698  dvcj  15700  plyf  15728  plyaddlem1  15738  plymullem1  15739  plyco  15750  plycj  15752  plycn  15753  plyrecj  15754  dvply2g  15757  efltlemlt  15765  sin0pilem2  15773  tangtx  15829  logdivlti  15872  rplogbval  15936  logbgcd1irraplemexp  15959  logbgcd1irraplemap  15960  logbgcd1irrap  15961  perfect1  15992  perfectlem1  15993  perfectlem2  15994  lgsval4a  16021  lgsdir2lem3  16029  lgsne0  16037  gausslemma2dlem3  16062  gausslemma2dlem4  16063  gausslemma2dlem6  16066  gausslemma2dlem7  16067  gausslemma2d  16068  lgseisenlem1  16069  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem2  16081  lgsquad3  16083  2lgsoddprmlem2  16105  2sqlem8a  16121  2sqlem8  16122  2sqlem9  16123  lpvtx  16200  upgrex  16224  upgr1een  16245  edgupgren  16262  umgredg  16266  upgrpredgv  16267  upgredg2vtx  16269  upgredgpr  16270  uspgrf1oedg  16297  usgredg4  16336  uspgredgdomord  16350  usgr1vr  16369  wlkvtxiedg  16466  wlkvtxiedgg  16467  wlk1walkdom  16480  upgriswlkdc  16481  upgrwlkedg  16482  uspgr2wlkeq  16486  uspgr2wlkeqi  16488  umgrwlknloop  16489  eupth2lem2dc  16580  trlsegvdeglem1  16581  eupth2lem3lem4fi  16594  bj-exlimmpi  16668  uzdcinzz  16696  bj-charfundcALT  16705  bj-2inf  16834  bj-peano4  16851  bj-nn0suc  16860  pw1ndom3  16890  subctctexmid  16900  exmidcon  16906  nninfalllem1  16912  nninfsellemqall  16919  nninfomnilem  16922  nninffeq  16924  nnnninfex  16926  exmidsbthrlem  16928  sbthomlem  16931  refeq  16934  isomninnlem  16940  apdifflemr  16957  redcwlpo  16966  reap0  16969  nconstwlpolem  16977