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  620  mt2d  625  mpjaod  718  stdcndcOLD  846  impidc  858  jadc  863  pm2.54dc  891  pm4.55dc  938  oplem1  975  mp3and  1340  xor3dc  1387  exlimdd  1872  exlimddv  1898  eqrdav  2176  necon1aidc  2398  necon1bidc  2399  necon4aidc  2415  reximddv  2580  reximssdv  2581  rexlimddv  2599  vtoclgft  2789  rspcedvd  2849  sseldd  3158  ssneldd  3160  tpid3g  3709  preq12b  3772  axpweq  4173  exmid1dc  4202  exmid1stab  4210  opth  4239  issod  4321  frirrg  4352  frind  4354  ralxfr2d  4466  rexxfr2d  4467  eldifpw  4479  onun2  4491  onuni  4495  elirr  4542  en2lp  4555  wetriext  4578  peano2  4596  relop  4779  elres  4945  sotri2  5028  iota4an  5199  iota5  5200  funeu  5243  funopg  5252  imadiflem  5297  funimaexglem  5301  ssimaex  5579  ffvelcdm  5651  dff3im  5663  dffo4  5666  f1eqcocnv  5794  f1oiso2  5830  riota5f  5857  riotass2  5859  acexmidlemcase  5872  ovmpodf  6008  ovmpodv2  6010  ovi3  6013  ov6g  6014  caoftrn  6110  op1steq  6182  tfr0dm  6325  tfrlemibxssdm  6330  tfrlemi14d  6336  tfr1onlembxssdm  6346  tfr1onlemaccex  6351  tfr1onlemres  6352  tfrcllembxssdm  6359  tfrcllemaccex  6364  tfrcllemres  6365  rdgivallem  6384  nnsucelsuc  6494  nnsucsssuc  6495  dcdifsnid  6507  nnawordex  6532  ersym  6549  mapvalg  6660  pmvalg  6661  mapsn  6692  fundmen  6808  mapdom1g  6849  fidceq  6871  fin0or  6888  findcard2  6891  findcard2s  6892  fiintim  6930  suplub2ti  7002  supsnti  7006  supisoex  7010  difinfsnlem  7100  difinfsn  7101  ctm  7110  ctssdclemn0  7111  ctssdccl  7112  ctssdc  7114  enumctlemm  7115  nnnninfeq2  7129  enomnilem  7138  exmidomniim  7141  exmidomni  7142  fodjuomnilemdc  7144  fodjuomnilemres  7148  omnimkv  7156  mkvprop  7158  omniwomnimkv  7167  en2eleq  7196  acfun  7208  exmidontriimlem1  7222  exmidontriimlem4  7225  exmidontriim  7226  ccfunen  7265  cc4f  7270  cc4n  7272  elni2  7315  mulclpi  7329  nlt1pig  7342  indpi  7343  recclnq  7393  ltexnqq  7409  halfnqq  7411  prarloclemarch  7419  prarloclemarch2  7420  prop  7476  prltlu  7488  prarloclem3step  7497  prarloclem5  7501  prarloclem  7502  prarloc  7504  prarloc2  7505  genpml  7518  genpmu  7519  genprndl  7522  genprndu  7523  genpdisj  7524  addnqprllem  7528  addnqprulem  7529  addlocprlemeq  7534  addlocprlemgt  7535  addlocprlem  7536  addlocpr  7537  nqprloc  7546  nqprl  7552  nqpru  7553  addnqprlemrl  7558  addnqprlemru  7559  appdivnq  7564  prmuloc  7567  prmuloc2  7568  mullocprlem  7571  mullocpr  7572  mulnqprlemrl  7574  mulnqprlemru  7575  ltprordil  7590  ltpopr  7596  ltsopr  7597  ltaddpr  7598  ltexprlemm  7601  ltexprlemopl  7602  ltexprlemlol  7603  ltexprlemopu  7604  ltexprlemupu  7605  ltexprlemloc  7608  ltexprlemfl  7610  ltexprlemrl  7611  ltexprlemfu  7612  ltexprlemru  7613  ltaprg  7620  recexprlemm  7625  recexprlem1ssl  7634  recexprlem1ssu  7635  aptiprleml  7640  aptiprlemu  7641  archpr  7644  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemupu  7650  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlemladdru  7657  cauappcvgprlem1  7660  archrecpr  7665  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemupu  7673  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemladdfu  7678  caucvgprlem1  7680  caucvgprlemlim  7682  caucvgprprlemnbj  7694  caucvgprprlemml  7695  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemopu  7700  caucvgprprlemupu  7701  caucvgprprlemdisj  7703  caucvgprprlemloc  7704  caucvgprprlemexbt  7707  caucvgprprlemaddq  7709  caucvgprprlemlim  7712  suplocexprlemss  7716  suplocexprlemrl  7718  suplocexprlemmu  7719  suplocexprlemru  7720  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemub  7724  suplocexprlemlub  7725  recexgt0sr  7774  mulgt0sr  7779  archsr  7783  caucvgsrlemoffcau  7799  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  cnm  7833  axarch  7892  axcaucvglemcau  7899  axpre-suploclemres  7902  lelttr  8048  ltletr  8049  ltled  8078  cnegexlem1  8134  cnegexlem2  8135  renegcl  8220  negf1o  8341  gt0add  8532  apreap  8546  apirr  8564  apsym  8565  apcotr  8566  apadd1  8567  apneg  8570  mulext1  8571  mulap0r  8574  apti  8581  aprcl  8605  aptap  8609  recexap  8612  mulap0  8613  receuap  8628  mul0eqap  8629  lep1  8804  lem1  8806  letrp1  8807  recreclt  8859  lbinf  8907  suprubex  8910  nnrecgt0  8959  bndndx  9177  nn0ge2m1nn  9238  elnn0z  9268  peano2z  9291  zaddcl  9295  ztri3or0  9297  zltnle  9301  zdceq  9330  zdcle  9331  zdclt  9332  zdiv  9343  zeo  9360  fnn0ind  9371  btwnz  9374  uzm1  9560  uzp1  9563  indstr  9595  supinfneg  9597  infsupneg  9598  eluzdc  9612  nn01to3  9619  qapne  9641  xrltled  9801  xrlelttr  9808  xrltletr  9809  ge0nemnf  9826  fzdcel  10042  elfzouz2  10163  fzoss1  10173  fzospliti  10178  fzocatel  10201  fzostep1  10239  qtri3or  10245  qltnle  10248  qdceq  10249  exbtwnzlemex  10252  rebtwn2zlemstep  10255  rebtwn2z  10257  qbtwnxr  10260  ioom  10263  ico0  10264  ioc0  10265  flqeqceilz  10320  modqadd1  10363  modqmul1  10379  frec2uzuzd  10404  frec2uzlt2d  10406  frec2uzf1od  10408  frecuzrdgrrn  10410  frec2uzrdg  10411  frecuzrdgrcl  10412  frecuzrdgsuc  10416  frecuzrdgrclt  10417  frecuzrdgdomlem  10419  uzsinds  10444  seqvalcd  10461  seqovcd  10465  seq3fveq2  10471  seq3shft2  10475  monoord  10478  seq3split  10481  seq3caopr3  10483  iseqf1olemab  10491  iseqf1olemnanb  10492  iseqf1olemqk  10496  seq3id3  10509  seq3id2  10511  seq3homo  10512  expgt1  10560  m1expeven  10569  expnbnd  10646  expnlbnd2  10648  nn0ltexp2  10691  apexp1  10700  hashennn  10762  zfz1isolem1  10822  seq3coll  10824  cjap  10917  caucvgre  10992  cvg1nlemres  10996  resqrexlemgt0  11031  resqrexlemglsq  11033  resqrexlemga  11034  resqrtcl  11040  abslt  11099  abssubap0  11101  abssubne0  11102  caubnd2  11128  qdenre  11213  maxabslemlub  11218  maxabs  11220  maxleast  11224  fimaxre2  11237  xrmaxiflemlub  11258  xrmaxif  11261  xrmaxltsup  11268  xrmaxadd  11271  xrmineqinf  11279  climuni  11303  2clim  11311  climcn1  11318  climcn2  11319  subcn2  11321  mulcn2  11322  climsqz  11345  climsqz2  11346  climcau  11357  climcvg1nlem  11359  climcaucn  11361  serf0  11362  sumrbdclem  11387  summodclem2  11392  zsumdc  11394  divcnv  11507  absltap  11519  absgtap  11520  mertenslem2  11546  ntrivcvgap  11558  prodrbdclem  11581  prodmodclem2  11587  zproddc  11589  prodssdc  11599  fprodsplitdc  11606  fprodcl2lem  11615  efcllemp  11668  tanvalap  11718  sin01bnd  11767  cos01bnd  11768  sin01gt0  11771  absef  11779  eirrap  11787  dvds0  11815  dvdsmul1  11822  dvdsmultr1d  11841  dvdslelemd  11851  divconjdvds  11857  alzdvds  11862  sqoddm1div8z  11893  nno  11913  divalglemex  11929  zsupcllemstep  11948  zsupcl  11950  infssuzledc  11953  dvdsbnd  11959  dvdslegcd  11967  zeqzmulgcd  11973  gcd0id  11982  gcdaddm  11987  gcd1  11990  gcdabs  11991  bezoutlemnewy  11999  bezoutlemstep  12000  bezoutlemmain  12001  bezoutlemex  12004  bezoutlemzz  12005  bezoutlemaz  12006  bezoutlembz  12007  bezoutlembi  12008  bezoutlemle  12011  bezoutlemsup  12012  mulgcd  12019  gcdzeq  12025  dvdsmulgcd  12028  sqgcd  12032  bezoutr1  12036  algcvga  12053  algfx  12054  eucalglt  12059  eucalg  12061  lcmneg  12076  lcmabs  12078  lcmgcdlem  12079  ncoprmgcdne1b  12091  mulgcddvds  12096  qredeq  12098  divgcdcoprm0  12103  cncongr1  12105  isprm2lem  12118  nprm  12125  dvdsnprmd  12127  prmdvdsfz  12141  isprm5lem  12143  coprm  12146  isprm6  12149  sqrt2irr  12164  pw2dvdslemn  12167  pw2dvdseulemle  12169  oddpwdclemdvds  12172  oddpwdclemndvds  12173  sqrt2irrap  12182  qnumdencl  12189  prmdiv  12237  modprmn0modprm0  12258  prm23lt5  12265  pythagtriplem4  12270  pythagtriplem19  12284  pythagtrip  12285  pclemub  12289  pcpre1  12294  pcpremul  12295  pceulem  12296  pcqcl  12308  pcidlem  12324  pcgcd1  12329  pc2dvds  12331  dvdsprmpweqle  12338  difsqpwdvds  12339  pcadd  12341  pcmpt  12343  expnprm  12353  pockthg  12357  infpnlem2  12360  prmunb  12362  1arith  12367  4sqlem10  12387  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemrnh  12419  ennnfonelemnn0  12425  ennnfonelemim  12427  exmidunben  12429  ctinfomlemom  12430  ctinfom  12431  ctinf  12433  omctfn  12446  nninfdclemp1  12453  setscomd  12505  imasaddfnlemg  12740  mhmf1o  12866  grpinveu  12916  grpasscan1  12938  dfgrp3mlem  12973  grp1inv  12982  issubg4m  13058  srgisid  13174  ringadd2  13215  ringinvnzdiv  13232  unitgrp  13290  ringelnzr  13333  lringuplu  13342  subrguss  13362  subrgintm  13369  aprcotr  13380  islmodd  13388  lssclg  13456  lss0cl  13460  lssvneln0  13464  lss1d  13475  tgcl  13603  neii1  13686  neii2  13688  neiss  13689  tpnei  13699  tgrest  13708  ssrest  13721  icnpimaex  13750  lmcvg  13756  cnpnei  13758  cnptopco  13761  lmff  13788  txcnp  13810  txcn  13814  hmeontr  13852  blssec  13977  mopni3  14023  blsscls2  14032  comet  14038  bdxmet  14040  bdmopn  14043  xmettxlem  14048  xmettx  14049  addcncntoplem  14090  mulc1cncf  14115  cncfco  14117  cncfmptc  14121  mulcncflem  14129  mulcncf  14130  dedekindeulemlu  14138  dedekindeulemeu  14139  suplociccreex  14141  suplociccex  14142  dedekindicclemlu  14147  dedekindicclemeu  14148  ivthinclemlopn  14153  ivthinclemlr  14154  ivthinclemuopn  14155  ivthinclemur  14156  ivthinclemloc  14158  ivthinc  14160  limcimolemlt  14172  limcresi  14174  cnplimcim  14175  cnplimclemle  14176  cnplimclemr  14177  limccnpcntop  14183  limccoap  14186  dvcoapbr  14210  dvcj  14212  efltlemlt  14234  sin0pilem2  14242  tangtx  14298  logdivlti  14341  rplogbval  14402  logbgcd1irraplemexp  14425  logbgcd1irraplemap  14426  logbgcd1irrap  14427  lgsval4a  14462  lgsdir2lem3  14470  lgsne0  14478  lgseisenlem1  14489  2lgsoddprmlem2  14493  2sqlem8a  14508  2sqlem8  14509  2sqlem9  14510  bj-exlimmpi  14561  uzdcinzz  14589  bj-charfundcALT  14600  bj-2inf  14729  bj-peano4  14746  bj-nn0suc  14755  subctctexmid  14789  nninfalllem1  14796  nninfsellemqall  14803  nninfomnilem  14806  nninffeq  14808  exmidsbthrlem  14809  sbthomlem  14812  refeq  14815  isomninnlem  14817  apdifflemr  14834  redcwlpo  14842  reap0  14845  nconstwlpolem  14851