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  1883  exlimddv  1910  eqrdav  2192  necon1aidc  2415  necon1bidc  2416  necon4aidc  2432  reximddv  2597  reximssdv  2598  rexlimddv  2616  vtoclgft  2811  rspcedvd  2871  sseldd  3181  ssneldd  3183  tpid3g  3734  preq12b  3797  axpweq  4201  exmid1dc  4230  exmid1stab  4238  opth  4267  issod  4351  frirrg  4382  frind  4384  ralxfr2d  4496  rexxfr2d  4497  eldifpw  4509  onun2  4523  onuni  4527  elirr  4574  en2lp  4587  wetriext  4610  peano2  4628  relop  4813  elres  4979  sotri2  5064  iota4an  5236  iota5  5237  funeu  5280  funopg  5289  imadiflem  5334  funimaexglem  5338  ssimaex  5619  ffvelcdm  5692  dff3im  5704  dffo4  5707  f1eqcocnv  5835  f1oiso2  5871  riota5f  5899  riotass2  5901  acexmidlemcase  5914  ovmpodf  6051  ovmpodv2  6053  ovi3  6057  ov6g  6058  caoftrn  6160  op1steq  6234  tfr0dm  6377  tfrlemibxssdm  6382  tfrlemi14d  6388  tfr1onlembxssdm  6398  tfr1onlemaccex  6403  tfr1onlemres  6404  tfrcllembxssdm  6411  tfrcllemaccex  6416  tfrcllemres  6417  rdgivallem  6436  nnsucelsuc  6546  nnsucsssuc  6547  dcdifsnid  6559  nnawordex  6584  ersym  6601  mapvalg  6714  pmvalg  6715  mapsn  6746  fundmen  6862  pw2f1odclem  6892  mapdom1g  6905  fidceq  6927  fin0or  6944  findcard2  6947  findcard2s  6948  fiintim  6987  suplub2ti  7062  supsnti  7066  supisoex  7070  difinfsnlem  7160  difinfsn  7161  ctm  7170  ctssdclemn0  7171  ctssdccl  7172  ctssdc  7174  enumctlemm  7175  nninfninc  7184  nnnninfeq2  7190  enomnilem  7199  exmidomniim  7202  exmidomni  7203  fodjuomnilemdc  7205  fodjuomnilemres  7209  omnimkv  7217  mkvprop  7219  omniwomnimkv  7228  en2eleq  7257  acfun  7269  exmidontriimlem1  7283  exmidontriimlem4  7286  exmidontriim  7287  ccfunen  7326  cc4f  7331  cc4n  7333  elni2  7376  mulclpi  7390  nlt1pig  7403  indpi  7404  recclnq  7454  ltexnqq  7470  halfnqq  7472  prarloclemarch  7480  prarloclemarch2  7481  prop  7537  prltlu  7549  prarloclem3step  7558  prarloclem5  7562  prarloclem  7563  prarloc  7565  prarloc2  7566  genpml  7579  genpmu  7580  genprndl  7583  genprndu  7584  genpdisj  7585  addnqprllem  7589  addnqprulem  7590  addlocprlemeq  7595  addlocprlemgt  7596  addlocprlem  7597  addlocpr  7598  nqprloc  7607  nqprl  7613  nqpru  7614  addnqprlemrl  7619  addnqprlemru  7620  appdivnq  7625  prmuloc  7628  prmuloc2  7629  mullocprlem  7632  mullocpr  7633  mulnqprlemrl  7635  mulnqprlemru  7636  ltprordil  7651  ltpopr  7657  ltsopr  7658  ltaddpr  7659  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  ltexprlemloc  7669  ltexprlemfl  7671  ltexprlemrl  7672  ltexprlemfu  7673  ltexprlemru  7674  ltaprg  7681  recexprlemm  7686  recexprlem1ssl  7695  recexprlem1ssu  7696  aptiprleml  7701  aptiprlemu  7702  archpr  7705  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemupu  7711  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  cauappcvgprlem1  7721  archrecpr  7726  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemupu  7734  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemladdfu  7739  caucvgprlem1  7741  caucvgprlemlim  7743  caucvgprprlemnbj  7755  caucvgprprlemml  7756  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemupu  7762  caucvgprprlemdisj  7764  caucvgprprlemloc  7765  caucvgprprlemexbt  7768  caucvgprprlemaddq  7770  caucvgprprlemlim  7773  suplocexprlemss  7777  suplocexprlemrl  7779  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  suplocexprlemlub  7786  recexgt0sr  7835  mulgt0sr  7840  archsr  7844  caucvgsrlemoffcau  7860  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  cnm  7894  axarch  7953  axcaucvglemcau  7960  axpre-suploclemres  7963  lelttr  8110  ltletr  8111  ltled  8140  cnegexlem1  8196  cnegexlem2  8197  renegcl  8282  negf1o  8403  gt0add  8594  apreap  8608  apirr  8626  apsym  8627  apcotr  8628  apadd1  8629  apneg  8632  mulext1  8633  mulap0r  8636  apti  8643  aprcl  8667  aptap  8671  recexap  8674  mulap0  8675  receuap  8690  mul0eqap  8691  lep1  8866  lem1  8868  letrp1  8869  recreclt  8921  lbinf  8969  suprubex  8972  nnrecgt0  9022  bndndx  9242  nn0ge2m1nn  9303  elnn0z  9333  peano2z  9356  zaddcl  9360  ztri3or0  9362  zltnle  9366  zdceq  9395  zdcle  9396  zdclt  9397  zdiv  9408  zeo  9425  fnn0ind  9436  btwnz  9439  uzm1  9626  uzp1  9629  indstr  9661  supinfneg  9663  infsupneg  9664  eluzdc  9678  nn01to3  9685  qapne  9707  xrltled  9868  xrlelttr  9875  xrltletr  9876  ge0nemnf  9893  fzdcel  10109  elfzouz2  10231  fzoss1  10241  fzospliti  10246  fzocatel  10269  fzostep1  10307  qtri3or  10313  qltnle  10316  qdceq  10317  qdclt  10318  exbtwnzlemex  10321  rebtwn2zlemstep  10324  rebtwn2z  10326  qbtwnxr  10329  ioom  10332  ico0  10333  ioc0  10334  flqeqceilz  10392  modqadd1  10435  modqmul1  10451  frec2uzuzd  10476  frec2uzlt2d  10478  frec2uzf1od  10480  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgdomlem  10491  uzsinds  10518  seqvalcd  10535  seqovcd  10541  seq3fveq2  10549  seqfveq2g  10551  seq3shft2  10555  seqshft2g  10556  monoord  10559  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  iseqf1olemab  10576  iseqf1olemnanb  10577  iseqf1olemqk  10581  seqf1oglem1  10593  seqf1og  10595  seq3id3  10598  seq3id2  10600  seq3homo  10601  seqhomog  10604  expgt1  10651  m1expeven  10660  expnbnd  10737  expnlbnd2  10739  nn0ltexp2  10783  apexp1  10792  hashennn  10854  zfz1isolem1  10914  seq3coll  10916  cjap  11053  caucvgre  11128  cvg1nlemres  11132  resqrexlemgt0  11167  resqrexlemglsq  11169  resqrexlemga  11170  resqrtcl  11176  abslt  11235  abssubap0  11237  abssubne0  11238  caubnd2  11264  qdenre  11349  maxabslemlub  11354  maxabs  11356  maxleast  11360  fimaxre2  11373  xrmaxiflemlub  11394  xrmaxif  11397  xrmaxltsup  11404  xrmaxadd  11407  xrmineqinf  11415  climuni  11439  2clim  11447  climcn1  11454  climcn2  11455  subcn2  11457  mulcn2  11458  climsqz  11481  climsqz2  11482  climcau  11493  climcvg1nlem  11495  climcaucn  11497  serf0  11498  sumrbdclem  11523  summodclem2  11528  zsumdc  11530  divcnv  11643  absltap  11655  absgtap  11656  mertenslem2  11682  ntrivcvgap  11694  prodrbdclem  11717  prodmodclem2  11723  zproddc  11725  prodssdc  11735  fprodsplitdc  11742  fprodcl2lem  11751  efcllemp  11804  tanvalap  11854  sin01bnd  11903  cos01bnd  11904  sin01gt0  11908  absef  11916  eirrap  11924  dvds0  11952  dvdsmul1  11959  dvdsmultr1d  11978  dvdslelemd  11988  divconjdvds  11994  alzdvds  11999  sqoddm1div8z  12030  nno  12050  divalglemex  12066  zsupcllemstep  12085  zsupcl  12087  infssuzledc  12090  dvdsbnd  12096  dvdslegcd  12104  zeqzmulgcd  12110  gcd0id  12119  gcdaddm  12124  gcd1  12127  gcdabs  12128  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlemex  12141  bezoutlemzz  12142  bezoutlemaz  12143  bezoutlembz  12144  bezoutlembi  12145  bezoutlemle  12148  bezoutlemsup  12149  mulgcd  12156  gcdzeq  12162  dvdsmulgcd  12165  sqgcd  12169  bezoutr1  12173  nninfctlemfo  12180  algcvga  12192  algfx  12193  eucalglt  12198  eucalg  12200  lcmneg  12215  lcmabs  12217  lcmgcdlem  12218  ncoprmgcdne1b  12230  mulgcddvds  12235  qredeq  12237  divgcdcoprm0  12242  cncongr1  12244  isprm2lem  12257  nprm  12264  dvdsnprmd  12266  prmdvdsfz  12280  isprm5lem  12282  coprm  12285  isprm6  12288  sqrt2irr  12303  pw2dvdslemn  12306  pw2dvdseulemle  12308  oddpwdclemdvds  12311  oddpwdclemndvds  12312  sqrt2irrap  12321  qnumdencl  12328  prmdiv  12376  modprmn0modprm0  12397  prm23lt5  12404  pythagtriplem4  12409  pythagtriplem19  12423  pythagtrip  12424  pclemub  12428  pcpre1  12433  pcpremul  12434  pceulem  12435  pcqcl  12447  pcidlem  12464  pcgcd1  12469  pc2dvds  12471  dvdsprmpweqle  12478  difsqpwdvds  12479  pcadd  12481  pcmpt  12484  expnprm  12494  pockthg  12498  infpnlem2  12501  prmunb  12503  1arith  12508  4sqlem10  12528  4sqlem11  12542  4sqlem12  12543  4sqlem13m  12544  4sqlem17  12548  4sqlem18  12549  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemrnh  12576  ennnfonelemnn0  12582  ennnfonelemim  12584  exmidunben  12586  ctinfomlemom  12587  ctinfom  12588  ctinf  12590  omctfn  12603  nninfdclemp1  12610  setscomd  12662  imasaddfnlemg  12900  mhmf1o  13045  grpinveu  13113  grpasscan1  13138  dfgrp3mlem  13173  grp1inv  13182  issubg4m  13266  ghmf1o  13348  srgisid  13485  ringadd2  13526  ringinvnzdiv  13549  unitgrp  13615  ringelnzr  13686  lringuplu  13695  subrguss  13735  subrgintm  13742  aprcotr  13784  islmodd  13792  lssclg  13863  lss0cl  13868  lssvneln0  13872  lss1d  13882  lmodindp1  13927  rnglidlmmgm  13995  znidomb  14157  znunit  14158  znrrg  14159  tgcl  14243  neii1  14326  neii2  14328  neiss  14329  tpnei  14339  tgrest  14348  ssrest  14361  icnpimaex  14390  lmcvg  14396  cnpnei  14398  cnptopco  14401  lmff  14428  txcnp  14450  txcn  14454  hmeontr  14492  blssec  14617  mopni3  14663  blsscls2  14672  comet  14678  bdxmet  14680  bdmopn  14683  xmettxlem  14688  xmettx  14689  addcncntoplem  14740  mpomulcn  14745  mulc1cncf  14768  cncfco  14770  cncfmptc  14775  mulcncflem  14786  mulcncf  14787  dedekindeulemlu  14800  dedekindeulemeu  14801  suplociccreex  14803  suplociccex  14804  dedekindicclemlu  14809  dedekindicclemeu  14810  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemloc  14820  ivthinc  14822  ivthreinc  14824  ivthdichlem  14830  limcimolemlt  14843  limcresi  14845  cnplimcim  14846  cnplimclemle  14847  cnplimclemr  14848  limccnpcntop  14854  limccoap  14857  dvcoapbr  14886  dvcj  14888  plyf  14916  plyaddlem1  14926  plymullem1  14927  plyco  14937  plycj  14939  plycn  14940  plyrecj  14941  efltlemlt  14950  sin0pilem2  14958  tangtx  15014  logdivlti  15057  rplogbval  15118  logbgcd1irraplemexp  15141  logbgcd1irraplemap  15142  logbgcd1irrap  15143  lgsval4a  15179  lgsdir2lem3  15187  lgsne0  15195  gausslemma2dlem3  15220  gausslemma2dlem4  15221  gausslemma2dlem6  15224  gausslemma2dlem7  15225  gausslemma2d  15226  lgseisenlem1  15227  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem2  15239  lgsquad3  15241  2lgsoddprmlem2  15263  2sqlem8a  15279  2sqlem8  15280  2sqlem9  15281  bj-exlimmpi  15332  uzdcinzz  15360  bj-charfundcALT  15371  bj-2inf  15500  bj-peano4  15517  bj-nn0suc  15526  1dom1el  15553  subctctexmid  15561  nninfalllem1  15568  nninfsellemqall  15575  nninfomnilem  15578  nninffeq  15580  exmidsbthrlem  15582  sbthomlem  15585  refeq  15588  isomninnlem  15590  apdifflemr  15607  redcwlpo  15615  reap0  15618  nconstwlpolem  15625