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  146  mpbird  166  jcai  309  mp2and  430  pm2.21dd  610  mt2d  615  mpjaod  708  stdcndcOLD  836  impidc  848  jadc  853  pm2.54dc  881  pm4.55dc  927  oplem1  964  mp3and  1329  xor3dc  1376  exlimdd  1859  exlimddv  1885  eqrdav  2163  necon1aidc  2385  necon1bidc  2386  necon4aidc  2402  reximddv  2567  reximssdv  2568  rexlimddv  2586  vtoclgft  2771  rspcedvd  2831  sseldd  3138  ssneldd  3140  tpid3g  3685  preq12b  3744  axpweq  4144  exmid1dc  4173  opth  4209  issod  4291  frirrg  4322  frind  4324  ralxfr2d  4436  rexxfr2d  4437  eldifpw  4449  onun2  4461  onuni  4465  elirr  4512  en2lp  4525  wetriext  4548  peano2  4566  relop  4748  elres  4914  sotri2  4995  iota4an  5166  iota5  5167  funeu  5207  funopg  5216  imadiflem  5261  funimaexglem  5265  ssimaex  5541  ffvelrn  5612  dff3im  5624  dffo4  5627  f1eqcocnv  5753  f1oiso2  5789  riota5f  5816  riotass2  5818  acexmidlemcase  5831  ovmpodf  5964  ovmpodv2  5966  ovi3  5969  ov6g  5970  caoftrn  6069  op1steq  6139  tfr0dm  6281  tfrlemibxssdm  6286  tfrlemi14d  6292  tfr1onlembxssdm  6302  tfr1onlemaccex  6307  tfr1onlemres  6308  tfrcllembxssdm  6315  tfrcllemaccex  6320  tfrcllemres  6321  rdgivallem  6340  nnsucelsuc  6450  nnsucsssuc  6451  dcdifsnid  6463  nnawordex  6487  ersym  6504  mapvalg  6615  pmvalg  6616  mapsn  6647  fundmen  6763  mapdom1g  6804  fidceq  6826  fin0or  6843  findcard2  6846  findcard2s  6847  fiintim  6885  suplub2ti  6957  supsnti  6961  supisoex  6965  difinfsnlem  7055  difinfsn  7056  ctm  7065  ctssdclemn0  7066  ctssdccl  7067  ctssdc  7069  enumctlemm  7070  nnnninfeq2  7084  enomnilem  7093  exmidomniim  7096  exmidomni  7097  fodjuomnilemdc  7099  fodjuomnilemres  7103  omnimkv  7111  mkvprop  7113  omniwomnimkv  7122  en2eleq  7142  acfun  7154  exmidontriimlem1  7168  exmidontriimlem4  7171  exmidontriim  7172  ccfunen  7196  cc4f  7201  cc4n  7203  elni2  7246  mulclpi  7260  nlt1pig  7273  indpi  7274  recclnq  7324  ltexnqq  7340  halfnqq  7342  prarloclemarch  7350  prarloclemarch2  7351  prop  7407  prltlu  7419  prarloclem3step  7428  prarloclem5  7432  prarloclem  7433  prarloc  7435  prarloc2  7436  genpml  7449  genpmu  7450  genprndl  7453  genprndu  7454  genpdisj  7455  addnqprllem  7459  addnqprulem  7460  addlocprlemeq  7465  addlocprlemgt  7466  addlocprlem  7467  addlocpr  7468  nqprloc  7477  nqprl  7483  nqpru  7484  addnqprlemrl  7489  addnqprlemru  7490  appdivnq  7495  prmuloc  7498  prmuloc2  7499  mullocprlem  7502  mullocpr  7503  mulnqprlemrl  7505  mulnqprlemru  7506  ltprordil  7521  ltpopr  7527  ltsopr  7528  ltaddpr  7529  ltexprlemm  7532  ltexprlemopl  7533  ltexprlemlol  7534  ltexprlemopu  7535  ltexprlemupu  7536  ltexprlemloc  7539  ltexprlemfl  7541  ltexprlemrl  7542  ltexprlemfu  7543  ltexprlemru  7544  ltaprg  7551  recexprlemm  7556  recexprlem1ssl  7565  recexprlem1ssu  7566  aptiprleml  7571  aptiprlemu  7572  archpr  7575  cauappcvgprlemm  7577  cauappcvgprlemopl  7578  cauappcvgprlemlol  7579  cauappcvgprlemopu  7580  cauappcvgprlemupu  7581  cauappcvgprlemdisj  7583  cauappcvgprlemloc  7584  cauappcvgprlemladdfu  7586  cauappcvgprlemladdfl  7587  cauappcvgprlemladdru  7588  cauappcvgprlem1  7591  archrecpr  7596  caucvgprlemnkj  7598  caucvgprlemnbj  7599  caucvgprlemm  7600  caucvgprlemopl  7601  caucvgprlemlol  7602  caucvgprlemopu  7603  caucvgprlemupu  7604  caucvgprlemdisj  7606  caucvgprlemloc  7607  caucvgprlemladdfu  7609  caucvgprlem1  7611  caucvgprlemlim  7613  caucvgprprlemnbj  7625  caucvgprprlemml  7626  caucvgprprlemopl  7629  caucvgprprlemlol  7630  caucvgprprlemopu  7631  caucvgprprlemupu  7632  caucvgprprlemdisj  7634  caucvgprprlemloc  7635  caucvgprprlemexbt  7638  caucvgprprlemaddq  7640  caucvgprprlemlim  7643  suplocexprlemss  7647  suplocexprlemrl  7649  suplocexprlemmu  7650  suplocexprlemru  7651  suplocexprlemdisj  7652  suplocexprlemloc  7653  suplocexprlemub  7655  suplocexprlemlub  7656  recexgt0sr  7705  mulgt0sr  7710  archsr  7714  caucvgsrlemoffcau  7730  suplocsrlemb  7738  suplocsrlempr  7739  suplocsrlem  7740  cnm  7764  axarch  7823  axcaucvglemcau  7830  axpre-suploclemres  7833  lelttr  7978  ltletr  7979  ltled  8008  cnegexlem1  8064  cnegexlem2  8065  renegcl  8150  negf1o  8271  gt0add  8462  apreap  8476  apirr  8494  apsym  8495  apcotr  8496  apadd1  8497  apneg  8500  mulext1  8501  mulap0r  8504  apti  8511  aprcl  8535  recexap  8541  mulap0  8542  receuap  8557  mul0eqap  8558  lep1  8731  lem1  8733  letrp1  8734  recreclt  8786  lbinf  8834  suprubex  8837  nnrecgt0  8886  bndndx  9104  nn0ge2m1nn  9165  elnn0z  9195  peano2z  9218  zaddcl  9222  ztri3or0  9224  zltnle  9228  zdceq  9257  zdcle  9258  zdclt  9259  zdiv  9270  zeo  9287  fnn0ind  9298  btwnz  9301  uzm1  9487  uzp1  9490  indstr  9522  supinfneg  9524  infsupneg  9525  eluzdc  9539  nn01to3  9546  qapne  9568  xrltled  9726  xrlelttr  9733  xrltletr  9734  ge0nemnf  9751  fzdcel  9965  elfzouz2  10086  fzoss1  10096  fzospliti  10101  fzocatel  10124  fzostep1  10162  qtri3or  10168  qltnle  10171  qdceq  10172  exbtwnzlemex  10175  rebtwn2zlemstep  10178  rebtwn2z  10180  qbtwnxr  10183  ioom  10186  ico0  10187  ioc0  10188  flqeqceilz  10243  modqadd1  10286  modqmul1  10302  frec2uzuzd  10327  frec2uzlt2d  10329  frec2uzf1od  10331  frecuzrdgrrn  10333  frec2uzrdg  10334  frecuzrdgrcl  10335  frecuzrdgsuc  10339  frecuzrdgrclt  10340  frecuzrdgdomlem  10342  uzsinds  10367  seqvalcd  10384  seqovcd  10388  seq3fveq2  10394  seq3shft2  10398  monoord  10401  seq3split  10404  seq3caopr3  10406  iseqf1olemab  10414  iseqf1olemnanb  10415  iseqf1olemqk  10419  seq3id3  10432  seq3id2  10434  seq3homo  10435  expgt1  10483  m1expeven  10492  expnbnd  10567  expnlbnd2  10569  nn0ltexp2  10612  apexp1  10620  hashennn  10682  zfz1isolem1  10739  seq3coll  10741  cjap  10834  caucvgre  10909  cvg1nlemres  10913  resqrexlemgt0  10948  resqrexlemglsq  10950  resqrexlemga  10951  resqrtcl  10957  abslt  11016  abssubap0  11018  abssubne0  11019  caubnd2  11045  qdenre  11130  maxabslemlub  11135  maxabs  11137  maxleast  11141  fimaxre2  11154  xrmaxiflemlub  11175  xrmaxif  11178  xrmaxltsup  11185  xrmaxadd  11188  xrmineqinf  11196  climuni  11220  2clim  11228  climcn1  11235  climcn2  11236  subcn2  11238  mulcn2  11239  climsqz  11262  climsqz2  11263  climcau  11274  climcvg1nlem  11276  climcaucn  11278  serf0  11279  sumrbdclem  11304  summodclem2  11309  zsumdc  11311  divcnv  11424  absltap  11436  absgtap  11437  mertenslem2  11463  ntrivcvgap  11475  prodrbdclem  11498  prodmodclem2  11504  zproddc  11506  prodssdc  11516  fprodsplitdc  11523  fprodcl2lem  11532  efcllemp  11585  tanvalap  11635  sin01bnd  11684  cos01bnd  11685  sin01gt0  11688  absef  11696  eirrap  11704  dvds0  11732  dvdsmul1  11739  dvdsmultr1d  11757  dvdslelemd  11766  divconjdvds  11772  alzdvds  11777  sqoddm1div8z  11808  nno  11828  divalglemex  11844  zsupcllemstep  11863  zsupcl  11865  infssuzledc  11868  dvdsbnd  11874  dvdslegcd  11882  zeqzmulgcd  11888  gcd0id  11897  gcdaddm  11902  gcd1  11905  gcdabs  11906  bezoutlemnewy  11914  bezoutlemstep  11915  bezoutlemmain  11916  bezoutlemex  11919  bezoutlemzz  11920  bezoutlemaz  11921  bezoutlembz  11922  bezoutlembi  11923  bezoutlemle  11926  bezoutlemsup  11927  mulgcd  11934  gcdzeq  11940  dvdsmulgcd  11943  sqgcd  11947  bezoutr1  11951  algcvga  11962  algfx  11963  eucalglt  11968  eucalg  11970  lcmneg  11985  lcmabs  11987  lcmgcdlem  11988  ncoprmgcdne1b  12000  mulgcddvds  12005  qredeq  12007  divgcdcoprm0  12012  cncongr1  12014  isprm2lem  12027  nprm  12034  dvdsnprmd  12036  prmdvdsfz  12050  coprm  12053  isprm6  12056  sqrt2irr  12071  pw2dvdslemn  12074  pw2dvdseulemle  12076  oddpwdclemdvds  12079  oddpwdclemndvds  12080  sqrt2irrap  12089  qnumdencl  12096  prmdiv  12144  modprmn0modprm0  12165  prm23lt5  12172  pythagtriplem4  12177  pythagtriplem19  12191  pythagtrip  12192  pclemub  12196  pcpre1  12201  pcpremul  12202  pceulem  12203  pcqcl  12215  pcidlem  12231  pcgcd1  12236  pc2dvds  12238  dvdsprmpweqle  12245  difsqpwdvds  12246  pcadd  12248  pcmpt  12250  expnprm  12260  ennnfonelemex  12284  ennnfonelemhom  12285  ennnfonelemrnh  12286  ennnfonelemnn0  12292  ennnfonelemim  12294  exmidunben  12296  ctinfomlemom  12297  ctinfom  12298  ctinf  12300  omctfn  12313  nninfdclemp1  12322  tgcl  12605  neii1  12688  neii2  12690  neiss  12691  tpnei  12701  tgrest  12710  ssrest  12723  icnpimaex  12752  lmcvg  12758  cnpnei  12760  cnptopco  12763  lmff  12790  txcnp  12812  txcn  12816  hmeontr  12854  blssec  12979  mopni3  13025  blsscls2  13034  comet  13040  bdxmet  13042  bdmopn  13045  xmettxlem  13050  xmettx  13051  addcncntoplem  13092  mulc1cncf  13117  cncfco  13119  cncfmptc  13123  mulcncflem  13131  mulcncf  13132  dedekindeulemlu  13140  dedekindeulemeu  13141  suplociccreex  13143  suplociccex  13144  dedekindicclemlu  13149  dedekindicclemeu  13150  ivthinclemlopn  13155  ivthinclemlr  13156  ivthinclemuopn  13157  ivthinclemur  13158  ivthinclemloc  13160  ivthinc  13162  limcimolemlt  13174  limcresi  13176  cnplimcim  13177  cnplimclemle  13178  cnplimclemr  13179  limccnpcntop  13185  limccoap  13188  dvcoapbr  13212  dvcj  13214  efltlemlt  13236  sin0pilem2  13244  tangtx  13300  logdivlti  13343  rplogbval  13404  logbgcd1irraplemexp  13427  logbgcd1irraplemap  13428  logbgcd1irrap  13429  bj-exlimmpi  13486  uzdcinzz  13514  bj-charfundcALT  13526  bj-2inf  13655  bj-peano4  13672  bj-nn0suc  13681  exmid1stab  13714  subctctexmid  13715  nninfalllem1  13722  nninfsellemqall  13729  nninfomnilem  13732  nninffeq  13734  exmidsbthrlem  13735  sbthomlem  13738  refeq  13741  isomninnlem  13743  apdifflemr  13760  redcwlpo  13768  reap0  13771  nconstwlpolem  13777