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  429  pm2.21dd  609  mt2d  614  mpjaod  707  stdcndcOLD  831  impidc  843  jadc  848  pm2.54dc  876  pm4.55dc  922  oplem1  959  mp3and  1318  xor3dc  1365  exlimdd  1844  exlimddv  1870  eqrdav  2138  necon1aidc  2359  necon1bidc  2360  necon4aidc  2376  reximddv  2535  reximssdv  2536  rexlimddv  2554  vtoclgft  2736  rspcedvd  2795  sseldd  3098  ssneldd  3100  tpid3g  3638  preq12b  3697  axpweq  4095  exmid1dc  4123  opth  4159  issod  4241  frirrg  4272  frind  4274  ralxfr2d  4385  rexxfr2d  4386  eldifpw  4398  onun2  4406  onuni  4410  elirr  4456  en2lp  4469  wetriext  4491  peano2  4509  relop  4689  elres  4855  sotri2  4936  iota4an  5107  iota5  5108  funeu  5148  funopg  5157  imadiflem  5202  funimaexglem  5206  ssimaex  5482  ffvelrn  5553  dff3im  5565  dffo4  5568  f1eqcocnv  5692  f1oiso2  5728  riota5f  5754  riotass2  5756  acexmidlemcase  5769  ovmpodf  5902  ovmpodv2  5904  ovi3  5907  ov6g  5908  caoftrn  6007  op1steq  6077  tfr0dm  6219  tfrlemibxssdm  6224  tfrlemi14d  6230  tfr1onlembxssdm  6240  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllembxssdm  6253  tfrcllemaccex  6258  tfrcllemres  6259  rdgivallem  6278  nnsucelsuc  6387  nnsucsssuc  6388  dcdifsnid  6400  nnawordex  6424  ersym  6441  mapvalg  6552  pmvalg  6553  mapsn  6584  fundmen  6700  mapdom1g  6741  fidceq  6763  fin0or  6780  findcard2  6783  findcard2s  6784  fiintim  6817  suplub2ti  6888  supsnti  6892  supisoex  6896  difinfsnlem  6984  difinfsn  6985  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumctlemm  6999  enomnilem  7010  exmidomniim  7013  exmidomni  7014  fodjuomnilemdc  7016  fodjuomnilemres  7020  omnimkv  7030  mkvprop  7032  en2eleq  7051  acfun  7063  ccfunen  7079  elni2  7122  mulclpi  7136  nlt1pig  7149  indpi  7150  recclnq  7200  ltexnqq  7216  halfnqq  7218  prarloclemarch  7226  prarloclemarch2  7227  prop  7283  prltlu  7295  prarloclem3step  7304  prarloclem5  7308  prarloclem  7309  prarloc  7311  prarloc2  7312  genpml  7325  genpmu  7326  genprndl  7329  genprndu  7330  genpdisj  7331  addnqprllem  7335  addnqprulem  7336  addlocprlemeq  7341  addlocprlemgt  7342  addlocprlem  7343  addlocpr  7344  nqprloc  7353  nqprl  7359  nqpru  7360  addnqprlemrl  7365  addnqprlemru  7366  appdivnq  7371  prmuloc  7374  prmuloc2  7375  mullocprlem  7378  mullocpr  7379  mulnqprlemrl  7381  mulnqprlemru  7382  ltprordil  7397  ltpopr  7403  ltsopr  7404  ltaddpr  7405  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemlol  7410  ltexprlemopu  7411  ltexprlemupu  7412  ltexprlemloc  7415  ltexprlemfl  7417  ltexprlemrl  7418  ltexprlemfu  7419  ltexprlemru  7420  ltaprg  7427  recexprlemm  7432  recexprlem1ssl  7441  recexprlem1ssu  7442  aptiprleml  7447  aptiprlemu  7448  archpr  7451  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemopu  7456  cauappcvgprlemupu  7457  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlem1  7467  archrecpr  7472  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemopu  7479  caucvgprlemupu  7480  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprlem1  7487  caucvgprlemlim  7489  caucvgprprlemnbj  7501  caucvgprprlemml  7502  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemopu  7507  caucvgprprlemupu  7508  caucvgprprlemdisj  7510  caucvgprprlemloc  7511  caucvgprprlemexbt  7514  caucvgprprlemaddq  7516  caucvgprprlemlim  7519  suplocexprlemss  7523  suplocexprlemrl  7525  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  suplocexprlemlub  7532  recexgt0sr  7581  mulgt0sr  7586  archsr  7590  caucvgsrlemoffcau  7606  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  cnm  7640  axarch  7699  axcaucvglemcau  7706  axpre-suploclemres  7709  lelttr  7852  ltletr  7853  ltled  7881  cnegexlem1  7937  cnegexlem2  7938  renegcl  8023  negf1o  8144  gt0add  8335  apreap  8349  apirr  8367  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  mulap0r  8377  apti  8384  aprcl  8408  recexap  8414  mulap0  8415  receuap  8430  mul0eqap  8431  lep1  8603  lem1  8605  letrp1  8606  recreclt  8658  lbinf  8706  suprubex  8709  nnrecgt0  8758  bndndx  8976  nn0ge2m1nn  9037  elnn0z  9067  peano2z  9090  zaddcl  9094  ztri3or0  9096  zltnle  9100  zdceq  9126  zdcle  9127  zdclt  9128  zdiv  9139  zeo  9156  fnn0ind  9167  btwnz  9170  uzm1  9356  uzp1  9359  indstr  9388  supinfneg  9390  infsupneg  9391  eluzdc  9404  nn01to3  9409  qapne  9431  xrltled  9585  xrlelttr  9589  xrltletr  9590  ge0nemnf  9607  fzdcel  9820  elfzouz2  9938  fzoss1  9948  fzospliti  9953  fzocatel  9976  fzostep1  10014  qtri3or  10020  qltnle  10023  qdceq  10024  exbtwnzlemex  10027  rebtwn2zlemstep  10030  rebtwn2z  10032  qbtwnxr  10035  ioom  10038  ico0  10039  ioc0  10040  flqeqceilz  10091  modqadd1  10134  modqmul1  10150  frec2uzuzd  10175  frec2uzlt2d  10177  frec2uzf1od  10179  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgdomlem  10190  uzsinds  10215  seqvalcd  10232  seqovcd  10236  seq3fveq2  10242  seq3shft2  10246  monoord  10249  seq3split  10252  seq3caopr3  10254  iseqf1olemab  10262  iseqf1olemnanb  10263  iseqf1olemqk  10267  seq3id3  10280  seq3id2  10282  seq3homo  10283  expgt1  10331  m1expeven  10340  expnbnd  10415  expnlbnd2  10417  hashennn  10526  zfz1isolem1  10583  seq3coll  10585  cjap  10678  caucvgre  10753  cvg1nlemres  10757  resqrexlemgt0  10792  resqrexlemglsq  10794  resqrexlemga  10795  resqrtcl  10801  abslt  10860  abssubap0  10862  abssubne0  10863  caubnd2  10889  qdenre  10974  maxabslemlub  10979  maxabs  10981  maxleast  10985  fimaxre2  10998  xrmaxiflemlub  11017  xrmaxif  11020  xrmaxltsup  11027  xrmaxadd  11030  xrmineqinf  11038  climuni  11062  2clim  11070  climcn1  11077  climcn2  11078  subcn2  11080  mulcn2  11081  climsqz  11104  climsqz2  11105  climcau  11116  climcvg1nlem  11118  climcaucn  11120  serf0  11121  sumrbdclem  11146  summodclem2  11151  zsumdc  11153  divcnv  11266  absltap  11278  absgtap  11279  mertenslem2  11305  ntrivcvgap  11317  prodrbdclem  11340  prodmodclem2  11346  efcllemp  11364  tanvalap  11415  sin01bnd  11464  cos01bnd  11465  sin01gt0  11468  absef  11476  eirrap  11484  dvds0  11508  dvdsmul1  11515  dvdsmultr1d  11532  dvdslelemd  11541  divconjdvds  11547  alzdvds  11552  sqoddm1div8z  11583  nno  11603  divalglemex  11619  zsupcllemstep  11638  zsupcl  11640  infssuzledc  11643  dvdsbnd  11645  dvdslegcd  11653  zeqzmulgcd  11659  gcd0id  11667  gcdaddm  11672  gcd1  11675  gcdabs  11676  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlemex  11689  bezoutlemzz  11690  bezoutlemaz  11691  bezoutlembz  11692  bezoutlembi  11693  bezoutlemle  11696  bezoutlemsup  11697  mulgcd  11704  gcdzeq  11710  dvdsmulgcd  11713  sqgcd  11717  bezoutr1  11721  algcvga  11732  algfx  11733  eucalglt  11738  eucalg  11740  lcmneg  11755  lcmabs  11757  lcmgcdlem  11758  ncoprmgcdne1b  11770  mulgcddvds  11775  qredeq  11777  divgcdcoprm0  11782  cncongr1  11784  isprm2lem  11797  nprm  11804  dvdsnprmd  11806  prmdvdsfz  11819  coprm  11822  isprm6  11825  sqrt2irr  11840  pw2dvdslemn  11843  pw2dvdseulemle  11845  oddpwdclemdvds  11848  oddpwdclemndvds  11849  sqrt2irrap  11858  qnumdencl  11865  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemrnh  11929  ennnfonelemnn0  11935  ennnfonelemim  11937  exmidunben  11939  ctinfomlemom  11940  ctinfom  11941  ctinf  11943  tgcl  12233  neii1  12316  neii2  12318  neiss  12319  tpnei  12329  tgrest  12338  ssrest  12351  icnpimaex  12380  lmcvg  12386  cnpnei  12388  cnptopco  12391  lmff  12418  txcnp  12440  txcn  12444  hmeontr  12482  blssec  12607  mopni3  12653  blsscls2  12662  comet  12668  bdxmet  12670  bdmopn  12673  xmettxlem  12678  xmettx  12679  addcncntoplem  12720  mulc1cncf  12745  cncfco  12747  cncfmptc  12751  mulcncflem  12759  mulcncf  12760  dedekindeulemlu  12768  dedekindeulemeu  12769  suplociccreex  12771  suplociccex  12772  dedekindicclemlu  12777  dedekindicclemeu  12778  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemloc  12788  ivthinc  12790  limcimolemlt  12802  limcresi  12804  cnplimcim  12805  cnplimclemle  12806  cnplimclemr  12807  limccnpcntop  12813  limccoap  12816  dvcoapbr  12840  dvcj  12842  sin0pilem2  12863  tangtx  12919  bj-exlimmpi  12977  uzdcinzz  13005  bj-2inf  13136  bj-peano4  13153  bj-nn0suc  13162  exmid1stab  13195  subctctexmid  13196  nninfalllem1  13203  nninfsellemqall  13211  nninfomnilem  13214  nninffeq  13216  exmidsbthrlem  13217  sbthomlem  13220  refeq  13223  isomninnlem  13225