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  7341  supsnti  7345  supisoex  7349  difinfsnlem  7439  difinfsn  7440  ctm  7449  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumctlemm  7454  nninfninc  7463  nnnninfeq2  7469  enomnilem  7478  exmidomniim  7481  exmidomni  7482  fodjuomnilemdc  7484  fodjuomnilemres  7488  omnimkv  7496  mkvprop  7498  omniwomnimkv  7507  en2prde  7539  pr2cv1  7541  en2eleq  7547  acfun  7563  exmidontriimlem1  7577  exmidontriimlem4  7580  exmidontriim  7581  papsym  7612  papcotr  7613  ccfunen  7630  cc4f  7635  cc4n  7637  elni2  7681  mulclpi  7695  nlt1pig  7708  indpi  7709  recclnq  7759  ltexnqq  7775  halfnqq  7777  prarloclemarch  7785  prarloclemarch2  7786  prop  7842  prltlu  7854  prarloclem3step  7863  prarloclem5  7867  prarloclem  7868  prarloc  7870  prarloc2  7871  genpml  7884  genpmu  7885  genprndl  7888  genprndu  7889  genpdisj  7890  addnqprllem  7894  addnqprulem  7895  addlocprlemeq  7900  addlocprlemgt  7901  addlocprlem  7902  addlocpr  7903  nqprloc  7912  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  appdivnq  7930  prmuloc  7933  prmuloc2  7934  mullocprlem  7937  mullocpr  7938  mulnqprlemrl  7940  mulnqprlemru  7941  ltprordil  7956  ltpopr  7962  ltsopr  7963  ltaddpr  7964  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  ltaprg  7986  recexprlemm  7991  recexprlem1ssl  8000  recexprlem1ssu  8001  aptiprleml  8006  aptiprlemu  8007  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlem1  8026  archrecpr  8031  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlem1  8046  caucvgprlemlim  8048  caucvgprprlemnbj  8060  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemupu  8067  caucvgprprlemdisj  8069  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlemlim  8078  suplocexprlemss  8082  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  recexgt0sr  8140  mulgt0sr  8145  archsr  8149  caucvgsrlemoffcau  8165  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  cnm  8199  axarch  8258  axcaucvglemcau  8265  axpre-suploclemres  8268  lelttr  8414  ltletr  8415  ltled  8446  cnegexlem1  8502  cnegexlem2  8503  renegcl  8588  negf1o  8710  gt0add  8903  apreap  8917  apirr  8935  apsym  8936  apcotr  8937  apadd1  8938  apneg  8941  mulext1  8942  mulap0r  8945  apti  8952  aprcl  8976  aptap  8980  recexap  8983  mulap0  8984  receuap  9001  mul0eqap  9002  lep1  9177  lem1  9179  letrp1  9180  recreclt  9232  lbinf  9280  suprubex  9283  nnrecgt0  9344  bndndx  9566  nn0ge2m1nn  9631  elnn0z  9661  peano2z  9684  zaddcl  9688  ztri3or0  9690  zltnle  9694  zdceq  9724  zdcle  9725  zdclt  9726  zdiv  9738  zeo  9755  fnn0ind  9766  btwnz  9769  uzm1  9962  uzp1  9965  indstr  10002  supinfneg  10004  infsupneg  10005  eluzdc  10019  nn01to3  10026  qapne  10048  xrltled  10211  xrlelttr  10218  xrltletr  10219  ge0nemnf  10236  fzdcel  10454  elfzouz2  10579  fzoss1  10590  fzospliti  10595  elincfzoext  10621  fzocatel  10627  fzostep1  10666  zsupcllemstep  10672  zsupcl  10674  infssuzledc  10677  qtri3or  10685  qltnle  10688  qdceq  10689  qdclt  10690  exbtwnzlemex  10694  rebtwn2zlemstep  10697  rebtwn2z  10699  qbtwnxr  10702  ioom  10705  ico0  10706  ioc0  10707  flqeqceilz  10768  modqadd1  10811  modqmul1  10827  frec2uzuzd  10852  frec2uzlt2d  10854  frec2uzf1od  10856  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgdomlem  10867  uzsinds  10894  seqvalcd  10911  seqovcd  10917  seq3fveq2  10925  seqfveq2g  10927  seq3shft2  10931  seqshft2g  10932  monoord  10935  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  iseqf1olemab  10952  iseqf1olemnanb  10953  iseqf1olemqk  10957  seqf1oglem1  10969  seqf1og  10971  seq3id3  10974  seq3id2  10976  seq3homo  10977  seqhomog  10980  expgt1  11027  m1expeven  11036  expnbnd  11114  expnlbnd2  11116  nn0ltexp2  11161  apexp1  11170  hashennn  11233  hashfibclem  11296  hashf1lem2  11300  zfz1isolem1  11306  seq3coll  11308  pfxwrdsymbg  11476  wrdind  11508  wrd2ind  11509  cjap  11686  caucvgre  11761  cvg1nlemres  11765  resqrexlemgt0  11800  resqrexlemglsq  11802  resqrexlemga  11803  resqrtcl  11809  abslt  11869  abssubap0  11871  abssubne0  11872  caubnd2  11898  qdenre  11983  maxabslemlub  11988  maxabs  11990  maxleast  11994  fimaxre2  12008  xrmaxiflemlub  12030  xrmaxif  12033  xrmaxltsup  12040  xrmaxadd  12043  xrmineqinf  12051  climuni  12075  2clim  12083  climcn1  12090  climcn2  12091  subcn2  12093  mulcn2  12094  climsqz  12117  climsqz2  12118  climcau  12129  climcvg1nlem  12131  climcaucn  12133  serf0  12134  sumrbdclem  12160  summodclem2  12165  zsumdc  12167  divcnv  12280  absltap  12292  absgtap  12293  mertenslem2  12319  ntrivcvgap  12331  prodrbdclem  12354  prodmodclem2  12360  zproddc  12362  prodssdc  12372  fprodsplitdc  12379  fprodcl2lem  12388  efcllemp  12441  tanvalap  12491  sin01bnd  12540  cos01bnd  12541  sin01gt0  12545  absef  12553  eirrap  12561  dvds0  12589  dvdsmul1  12596  dvdsmultr1d  12615  dvdslelemd  12626  divconjdvds  12632  alzdvds  12637  3dvds  12647  sqoddm1div8z  12669  nno  12689  divalglemex  12705  bits0o  12733  dvdsbnd  12749  dvdslegcd  12757  zeqzmulgcd  12763  gcd0id  12772  gcdaddm  12777  gcd1  12780  gcdabs  12781  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlemex  12794  bezoutlemzz  12795  bezoutlemaz  12796  bezoutlembz  12797  bezoutlembi  12798  bezoutlemle  12801  bezoutlemsup  12802  mulgcd  12809  gcdzeq  12815  dvdsmulgcd  12818  sqgcd  12822  bezoutr1  12826  nninfctlemfo  12833  algcvga  12845  algfx  12846  eucalglt  12851  eucalg  12853  lcmneg  12868  lcmabs  12870  lcmgcdlem  12871  ncoprmgcdne1b  12883  mulgcddvds  12888  qredeq  12890  divgcdcoprm0  12895  cncongr1  12897  isprm2lem  12910  nprm  12917  dvdsnprmd  12919  prmdvdsfz  12934  isprm5lem  12936  coprm  12939  isprm6  12942  sqrt2irr  12957  pwbdvdslemn  12960  pwbdvdseulemle  12962  nnmaxpwlemdvds  12965  nnmaxpwlemndvds  12966  sqrt2irrap  12976  qnumdencl  12983  nn0sqdcq  13004  sqrtrirr  13005  prmdiv  13033  modprmn0modprm0  13055  prm23lt5  13062  pythagtriplem4  13067  pythagtriplem19  13081  pythagtrip  13082  pclemub  13086  pcpre1  13091  pcpremul  13092  pceulem  13093  pcqcl  13105  pcidlem  13122  pcgcd1  13127  pc2dvds  13129  dvdsprmpweqle  13136  difsqpwdvds  13137  pcadd  13139  pcmpt  13142  expnprm  13152  pockthg  13156  infpnlem2  13159  prmunb  13161  1arith  13166  4sqlem10  13186  4sqlem11  13200  4sqlem12  13201  4sqlem13m  13202  4sqlem17  13206  4sqlem18  13207  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemfrceq  13321  ennnfonelemex  13354  ennnfonelemhom  13355  ennnfonelemrnh  13356  ennnfonelemnn0  13362  ennnfonelemim  13364  exmidunben  13366  ctinfomlemom  13367  ctinfom  13368  ctinf  13370  omctfn  13383  nninfdclemp1  13390  setscomd  13442  imasaddfnlemg  13684  mhmf1o  13826  grpinveu  13892  grpasscan1  13917  dfgrp3mlem  13952  grp1inv  13961  issubg4m  14045  ghmf1o  14127  srgisid  14339  ringadd2  14381  ringinvnzdiv  14404  unitgrp  14472  ringelnzr  14543  lringuplu  14552  subrguss  14593  subrgintm  14600  aprcotr  14646  islmodd  14678  lssclg  14750  lss0cl  14755  lssvneln0  14759  lss1d  14769  lmodindp1  14814  rnglidlmmgm  14882  znidomb  15042  znunit  15043  znrrg  15044  rnasclassa  15087  mplsubgfilemcl  15139  mplsubgfileminv  15140  tgcl  15214  neii1  15297  neii2  15299  neiss  15300  tpnei  15310  tgrest  15319  ssrest  15332  icnpimaex  15361  lmcvg  15367  cnpnei  15369  cnptopco  15372  lmff  15399  txcnp  15421  txcn  15425  hmeontr  15463  blssec  15588  mopni3  15634  blsscls2  15643  comet  15649  bdxmet  15651  bdmopn  15654  xmettxlem  15659  xmettx  15660  addcncntoplem  15711  mpomulcn  15716  mulc1cncf  15739  cncfco  15741  cncfmptc  15746  mulcncflem  15757  mulcncf  15758  dedekindeulemlu  15771  dedekindeulemeu  15772  suplociccreex  15774  suplociccex  15775  dedekindicclemlu  15780  dedekindicclemeu  15781  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemloc  15791  ivthinc  15793  ivthreinc  15795  ivthdichlem  15801  limcimolemlt  15814  limcresi  15816  cnplimcim  15817  cnplimclemle  15818  cnplimclemr  15819  limccnpcntop  15825  limccoap  15828  dvcoapbr  15857  dvcj  15859  plyf  15887  plyaddlem1  15897  plymullem1  15898  plyco  15909  plycj  15911  plycn  15912  plyrecj  15913  dvply2g  15916  efltlemlt  15924  sin0pilem2  15933  tangtx  15989  logdivlti  16033  logdivlt  16046  rplogbval  16100  logbgcd1irraplemexp  16123  logbgcd1irraplemap  16124  logbgcd1irrap  16125  zprmlogbaplem2  16135  zprmlogbap  16137  birthdaylem1g  16144  ppiublem2  16193  perfect1  16196  perfectlem1  16197  perfectlem2  16198  lgsval4a  16239  lgsdir2lem3  16247  lgsne0  16255  gausslemma2dlem3  16280  gausslemma2dlem4  16281  gausslemma2dlem6  16284  gausslemma2dlem7  16285  gausslemma2d  16286  lgseisenlem1  16287  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem2  16299  lgsquad3  16301  2lgsoddprmlem2  16323  2sqlem8a  16339  2sqlem8  16340  2sqlem9  16341  lpvtx  16418  upgrex  16442  upgr1een  16463  edgupgren  16480  umgredg  16484  upgrpredgv  16485  upgredg2vtx  16487  upgredgpr  16488  uspgrf1oedg  16515  usgredg4  16554  uspgredgdomord  16568  usgr1vr  16587  wlkvtxiedg  16684  wlkvtxiedgg  16685  wlk1walkdom  16698  upgriswlkdc  16699  upgrwlkedg  16700  uspgr2wlkeq  16704  uspgr2wlkeqi  16706  umgrwlknloop  16707  eupth2lem2dc  16798  trlsegvdeglem1  16799  eupth2lem3lem4fi  16812  bj-exlimmpi  16896  uzdcinzz  16924  bj-charfundcALT  16933  bj-2inf  17062  bj-peano4  17079  bj-nn0suc  17088  pw1ndom3  17118  subctctexmid  17128  exmidcon  17135  nninfalllem1  17149  nninfsellemqall  17156  nninfomnilem  17159  nninffeq  17161  nnnninfex  17163  exmidsbthrlem  17165  sbthomlem  17168  refeq  17171  isomninnlem  17177  apdifflemr  17194  redcwlpo  17203  reap0  17206  nconstwlpolem  17213