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  3185  ssneldd  3187  tpid3g  3738  preq12b  3801  axpweq  4205  exmid1dc  4234  exmid1stab  4242  opth  4271  issod  4355  frirrg  4386  frind  4388  ralxfr2d  4500  rexxfr2d  4501  eldifpw  4513  onun2  4527  onuni  4531  elirr  4578  en2lp  4591  wetriext  4614  peano2  4632  relop  4817  elres  4983  sotri2  5068  iota4an  5240  iota5  5241  funeu  5284  funopg  5293  imadiflem  5338  funimaexglem  5342  ssimaex  5623  ffvelcdm  5696  dff3im  5708  dffo4  5711  f1eqcocnv  5839  f1oiso2  5875  riota5f  5903  riotass2  5905  acexmidlemcase  5918  ovmpodf  6055  ovmpodv2  6057  ovi3  6061  ov6g  6062  caoftrn  6164  op1steq  6238  tfr0dm  6381  tfrlemibxssdm  6386  tfrlemi14d  6392  tfr1onlembxssdm  6402  tfr1onlemaccex  6407  tfr1onlemres  6408  tfrcllembxssdm  6415  tfrcllemaccex  6420  tfrcllemres  6421  rdgivallem  6440  nnsucelsuc  6550  nnsucsssuc  6551  dcdifsnid  6563  nnawordex  6588  ersym  6605  mapvalg  6718  pmvalg  6719  mapsn  6750  fundmen  6866  pw2f1odclem  6896  mapdom1g  6909  fidceq  6931  fin0or  6948  findcard2  6951  findcard2s  6952  prfidceq  6990  fiintim  6993  suplub2ti  7068  supsnti  7072  supisoex  7076  difinfsnlem  7166  difinfsn  7167  ctm  7176  ctssdclemn0  7177  ctssdccl  7178  ctssdc  7180  enumctlemm  7181  nninfninc  7190  nnnninfeq2  7196  enomnilem  7205  exmidomniim  7208  exmidomni  7209  fodjuomnilemdc  7211  fodjuomnilemres  7215  omnimkv  7223  mkvprop  7225  omniwomnimkv  7234  en2eleq  7264  acfun  7276  exmidontriimlem1  7290  exmidontriimlem4  7293  exmidontriim  7294  ccfunen  7333  cc4f  7338  cc4n  7340  elni2  7383  mulclpi  7397  nlt1pig  7410  indpi  7411  recclnq  7461  ltexnqq  7477  halfnqq  7479  prarloclemarch  7487  prarloclemarch2  7488  prop  7544  prltlu  7556  prarloclem3step  7565  prarloclem5  7569  prarloclem  7570  prarloc  7572  prarloc2  7573  genpml  7586  genpmu  7587  genprndl  7590  genprndu  7591  genpdisj  7592  addnqprllem  7596  addnqprulem  7597  addlocprlemeq  7602  addlocprlemgt  7603  addlocprlem  7604  addlocpr  7605  nqprloc  7614  nqprl  7620  nqpru  7621  addnqprlemrl  7626  addnqprlemru  7627  appdivnq  7632  prmuloc  7635  prmuloc2  7636  mullocprlem  7639  mullocpr  7640  mulnqprlemrl  7642  mulnqprlemru  7643  ltprordil  7658  ltpopr  7664  ltsopr  7665  ltaddpr  7666  ltexprlemm  7669  ltexprlemopl  7670  ltexprlemlol  7671  ltexprlemopu  7672  ltexprlemupu  7673  ltexprlemloc  7676  ltexprlemfl  7678  ltexprlemrl  7679  ltexprlemfu  7680  ltexprlemru  7681  ltaprg  7688  recexprlemm  7693  recexprlem1ssl  7702  recexprlem1ssu  7703  aptiprleml  7708  aptiprlemu  7709  archpr  7712  cauappcvgprlemm  7714  cauappcvgprlemopl  7715  cauappcvgprlemlol  7716  cauappcvgprlemopu  7717  cauappcvgprlemupu  7718  cauappcvgprlemdisj  7720  cauappcvgprlemloc  7721  cauappcvgprlemladdfu  7723  cauappcvgprlemladdfl  7724  cauappcvgprlemladdru  7725  cauappcvgprlem1  7728  archrecpr  7733  caucvgprlemnkj  7735  caucvgprlemnbj  7736  caucvgprlemm  7737  caucvgprlemopl  7738  caucvgprlemlol  7739  caucvgprlemopu  7740  caucvgprlemupu  7741  caucvgprlemdisj  7743  caucvgprlemloc  7744  caucvgprlemladdfu  7746  caucvgprlem1  7748  caucvgprlemlim  7750  caucvgprprlemnbj  7762  caucvgprprlemml  7763  caucvgprprlemopl  7766  caucvgprprlemlol  7767  caucvgprprlemopu  7768  caucvgprprlemupu  7769  caucvgprprlemdisj  7771  caucvgprprlemloc  7772  caucvgprprlemexbt  7775  caucvgprprlemaddq  7777  caucvgprprlemlim  7780  suplocexprlemss  7784  suplocexprlemrl  7786  suplocexprlemmu  7787  suplocexprlemru  7788  suplocexprlemdisj  7789  suplocexprlemloc  7790  suplocexprlemub  7792  suplocexprlemlub  7793  recexgt0sr  7842  mulgt0sr  7847  archsr  7851  caucvgsrlemoffcau  7867  suplocsrlemb  7875  suplocsrlempr  7876  suplocsrlem  7877  cnm  7901  axarch  7960  axcaucvglemcau  7967  axpre-suploclemres  7970  lelttr  8117  ltletr  8118  ltled  8147  cnegexlem1  8203  cnegexlem2  8204  renegcl  8289  negf1o  8410  gt0add  8602  apreap  8616  apirr  8634  apsym  8635  apcotr  8636  apadd1  8637  apneg  8640  mulext1  8641  mulap0r  8644  apti  8651  aprcl  8675  aptap  8679  recexap  8682  mulap0  8683  receuap  8698  mul0eqap  8699  lep1  8874  lem1  8876  letrp1  8877  recreclt  8929  lbinf  8977  suprubex  8980  nnrecgt0  9030  bndndx  9250  nn0ge2m1nn  9311  elnn0z  9341  peano2z  9364  zaddcl  9368  ztri3or0  9370  zltnle  9374  zdceq  9403  zdcle  9404  zdclt  9405  zdiv  9416  zeo  9433  fnn0ind  9444  btwnz  9447  uzm1  9634  uzp1  9637  indstr  9669  supinfneg  9671  infsupneg  9672  eluzdc  9686  nn01to3  9693  qapne  9715  xrltled  9876  xrlelttr  9883  xrltletr  9884  ge0nemnf  9901  fzdcel  10117  elfzouz2  10239  fzoss1  10249  fzospliti  10254  fzocatel  10277  fzostep1  10315  zsupcllemstep  10321  zsupcl  10323  infssuzledc  10326  qtri3or  10332  qltnle  10335  qdceq  10336  qdclt  10337  exbtwnzlemex  10341  rebtwn2zlemstep  10344  rebtwn2z  10346  qbtwnxr  10349  ioom  10352  ico0  10353  ioc0  10354  flqeqceilz  10412  modqadd1  10455  modqmul1  10471  frec2uzuzd  10496  frec2uzlt2d  10498  frec2uzf1od  10500  frecuzrdgrrn  10502  frec2uzrdg  10503  frecuzrdgrcl  10504  frecuzrdgsuc  10508  frecuzrdgrclt  10509  frecuzrdgdomlem  10511  uzsinds  10538  seqvalcd  10555  seqovcd  10561  seq3fveq2  10569  seqfveq2g  10571  seq3shft2  10575  seqshft2g  10576  monoord  10579  seq3split  10582  seqsplitg  10583  seq3caopr3  10585  iseqf1olemab  10596  iseqf1olemnanb  10597  iseqf1olemqk  10601  seqf1oglem1  10613  seqf1og  10615  seq3id3  10618  seq3id2  10620  seq3homo  10621  seqhomog  10624  expgt1  10671  m1expeven  10680  expnbnd  10757  expnlbnd2  10759  nn0ltexp2  10803  apexp1  10812  hashennn  10874  zfz1isolem1  10934  seq3coll  10936  cjap  11073  caucvgre  11148  cvg1nlemres  11152  resqrexlemgt0  11187  resqrexlemglsq  11189  resqrexlemga  11190  resqrtcl  11196  abslt  11255  abssubap0  11257  abssubne0  11258  caubnd2  11284  qdenre  11369  maxabslemlub  11374  maxabs  11376  maxleast  11380  fimaxre2  11394  xrmaxiflemlub  11415  xrmaxif  11418  xrmaxltsup  11425  xrmaxadd  11428  xrmineqinf  11436  climuni  11460  2clim  11468  climcn1  11475  climcn2  11476  subcn2  11478  mulcn2  11479  climsqz  11502  climsqz2  11503  climcau  11514  climcvg1nlem  11516  climcaucn  11518  serf0  11519  sumrbdclem  11544  summodclem2  11549  zsumdc  11551  divcnv  11664  absltap  11676  absgtap  11677  mertenslem2  11703  ntrivcvgap  11715  prodrbdclem  11738  prodmodclem2  11744  zproddc  11746  prodssdc  11756  fprodsplitdc  11763  fprodcl2lem  11772  efcllemp  11825  tanvalap  11875  sin01bnd  11924  cos01bnd  11925  sin01gt0  11929  absef  11937  eirrap  11945  dvds0  11973  dvdsmul1  11980  dvdsmultr1d  11999  dvdslelemd  12010  divconjdvds  12016  alzdvds  12021  3dvds  12031  sqoddm1div8z  12053  nno  12073  divalglemex  12089  bits0o  12117  dvdsbnd  12133  dvdslegcd  12141  zeqzmulgcd  12147  gcd0id  12156  gcdaddm  12161  gcd1  12164  gcdabs  12165  bezoutlemnewy  12173  bezoutlemstep  12174  bezoutlemmain  12175  bezoutlemex  12178  bezoutlemzz  12179  bezoutlemaz  12180  bezoutlembz  12181  bezoutlembi  12182  bezoutlemle  12185  bezoutlemsup  12186  mulgcd  12193  gcdzeq  12199  dvdsmulgcd  12202  sqgcd  12206  bezoutr1  12210  nninfctlemfo  12217  algcvga  12229  algfx  12230  eucalglt  12235  eucalg  12237  lcmneg  12252  lcmabs  12254  lcmgcdlem  12255  ncoprmgcdne1b  12267  mulgcddvds  12272  qredeq  12274  divgcdcoprm0  12279  cncongr1  12281  isprm2lem  12294  nprm  12301  dvdsnprmd  12303  prmdvdsfz  12317  isprm5lem  12319  coprm  12322  isprm6  12325  sqrt2irr  12340  pw2dvdslemn  12343  pw2dvdseulemle  12345  oddpwdclemdvds  12348  oddpwdclemndvds  12349  sqrt2irrap  12358  qnumdencl  12365  prmdiv  12413  modprmn0modprm0  12435  prm23lt5  12442  pythagtriplem4  12447  pythagtriplem19  12461  pythagtrip  12462  pclemub  12466  pcpre1  12471  pcpremul  12472  pceulem  12473  pcqcl  12485  pcidlem  12502  pcgcd1  12507  pc2dvds  12509  dvdsprmpweqle  12516  difsqpwdvds  12517  pcadd  12519  pcmpt  12522  expnprm  12532  pockthg  12536  infpnlem2  12539  prmunb  12541  1arith  12546  4sqlem10  12566  4sqlem11  12580  4sqlem12  12581  4sqlem13m  12582  4sqlem17  12586  4sqlem18  12587  ennnfonelemex  12641  ennnfonelemhom  12642  ennnfonelemrnh  12643  ennnfonelemnn0  12649  ennnfonelemim  12651  exmidunben  12653  ctinfomlemom  12654  ctinfom  12655  ctinf  12657  omctfn  12670  nninfdclemp1  12677  setscomd  12729  imasaddfnlemg  12967  mhmf1o  13112  grpinveu  13180  grpasscan1  13205  dfgrp3mlem  13240  grp1inv  13249  issubg4m  13333  ghmf1o  13415  srgisid  13552  ringadd2  13593  ringinvnzdiv  13616  unitgrp  13682  ringelnzr  13753  lringuplu  13762  subrguss  13802  subrgintm  13809  aprcotr  13851  islmodd  13859  lssclg  13930  lss0cl  13935  lssvneln0  13939  lss1d  13949  lmodindp1  13994  rnglidlmmgm  14062  znidomb  14224  znunit  14225  znrrg  14226  tgcl  14310  neii1  14393  neii2  14395  neiss  14396  tpnei  14406  tgrest  14415  ssrest  14428  icnpimaex  14457  lmcvg  14463  cnpnei  14465  cnptopco  14468  lmff  14495  txcnp  14517  txcn  14521  hmeontr  14559  blssec  14684  mopni3  14730  blsscls2  14739  comet  14745  bdxmet  14747  bdmopn  14750  xmettxlem  14755  xmettx  14756  addcncntoplem  14807  mpomulcn  14812  mulc1cncf  14835  cncfco  14837  cncfmptc  14842  mulcncflem  14853  mulcncf  14854  dedekindeulemlu  14867  dedekindeulemeu  14868  suplociccreex  14870  suplociccex  14871  dedekindicclemlu  14876  dedekindicclemeu  14877  ivthinclemlopn  14882  ivthinclemlr  14883  ivthinclemuopn  14884  ivthinclemur  14885  ivthinclemloc  14887  ivthinc  14889  ivthreinc  14891  ivthdichlem  14897  limcimolemlt  14910  limcresi  14912  cnplimcim  14913  cnplimclemle  14914  cnplimclemr  14915  limccnpcntop  14921  limccoap  14924  dvcoapbr  14953  dvcj  14955  plyf  14983  plyaddlem1  14993  plymullem1  14994  plyco  15005  plycj  15007  plycn  15008  plyrecj  15009  dvply2g  15012  efltlemlt  15020  sin0pilem2  15028  tangtx  15084  logdivlti  15127  rplogbval  15191  logbgcd1irraplemexp  15214  logbgcd1irraplemap  15215  logbgcd1irrap  15216  perfect1  15244  perfectlem1  15245  perfectlem2  15246  lgsval4a  15273  lgsdir2lem3  15281  lgsne0  15289  gausslemma2dlem3  15314  gausslemma2dlem4  15315  gausslemma2dlem6  15318  gausslemma2dlem7  15319  gausslemma2d  15320  lgseisenlem1  15321  lgsquadlem2  15329  lgsquadlem3  15330  lgsquad2lem2  15333  lgsquad3  15335  2lgsoddprmlem2  15357  2sqlem8a  15373  2sqlem8  15374  2sqlem9  15375  bj-exlimmpi  15426  uzdcinzz  15454  bj-charfundcALT  15465  bj-2inf  15594  bj-peano4  15611  bj-nn0suc  15620  1dom1el  15647  subctctexmid  15655  nninfalllem1  15662  nninfsellemqall  15669  nninfomnilem  15672  nninffeq  15674  exmidsbthrlem  15676  sbthomlem  15679  refeq  15682  isomninnlem  15684  apdifflemr  15701  redcwlpo  15709  reap0  15712  nconstwlpolem  15719