Theorem mpd 46

Description: A modus ponens deduction.

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 8	. 2 |- ((ph -> ps) -> (ph -> ch))
4	1, 3	ax-mp 6	1 |- (ph -> ch)

Syntax hints:   -> wi 2

This theorem is referenced by:  mpdd 47  mpcom 49  sylc 62  mtod 95  mt2d 98  mt3d 101  mpbid 170  mpbird 171  jcai 237  mpand 524  mp2and 526  mpdan 527  pclem6 555  ecase2d 558  mopick2 1057  sseldd 1507  preq12b 1874  reuuni4 1959  ordtri3or 2230  ordunidif 2260  ordtri2or2 2329  ordun 2332  suc11 2341  limsuc 2361  limsssuc 2362  nnlim 2385  nnsuc 2389  peano5 2394  fssxp 2761  fnfvbr 2855  ffvrn 2890  fopab2 2891  isofrlem 2939  tz7.49 2997  oalimcl 3162  oaass 3163  nnarcl 3174  omsmolem 3195  mapvalg 3263  mapsn 3269  f1imaen 3327  fundmen 3333  mapxpen 3390  omsdomnn 3424  ssnn 3429  ssfi 3430  unblem3 3433  isfinite2 3437  unfilem3 3440  unfi2 3442  fiint 3445  inf3lem5 3468  aceq5 3563  zornlem7 3609  fodom 3613  imadomg 3616  cardnn 3631  sucdom 3648  cardlim 3657  cardaleph 3690  indpi 3828  nsmallpq 3877  prnmadd 3894  genpnnp 3902  genpnmax 3904  prlem934b 3932  prlem934 3933  ltaddpr 3934  ltexprlem2 3937  ltexprlem7 3942  prlem936 3949  reclem2pr 3951  suppsr2 4017  suppsr3 4018  supsrlem2 4020  axnegex 4078  axrnegex 4080  negeu 4124  receu 4215  nn2get 4438  nnrecgt0t 4447  nndiv 4453  rimul 4534  elnnz1 4581  zltp1let 4597  btwnz 4613  uzwo3lem1 4614  qbtwnre 4650  uzrdgsuc 4659  seqrn 4673  sqrlem12 4742  sqr2irr 4782  replimt 4798  infxpidmlem11 4943  infxpidmlem12 4944  infdif 4948  hlimcaui 5141  ocorth 5172  projlem25 5217  projlem26 5218  projlem31 5223  pjthlem11 5235  omlsi 5250  pjpj0 5259  osumlem7 5536  spansncv 5542  5oalem6 5549  strlem6 5697  stcltrlem2 5710  atcveq0 5746  atexch 5769  atcvat 5771  mdsymlem1 5776  mdsymlem3 5778  mdsymlem5 5780  sumdmdlem 5786

This theorem was proved from axioms:  ax-2 4  ax-mp 6

metamath.org