Theorem pm2.43d 59

Description: Deduction absorbing redundant antecedent.

Hypothesis

Ref	Expression
pm2.43d.1	|- (ph -> (ps -> (ps -> ch)))

Assertion

Ref	Expression
pm2.43d	|- (ph -> (ps -> ch))

Proof of Theorem pm2.43d

Step	Hyp	Ref	Expression
1		pm2.43d.1	. 2 |- (ph -> (ps -> (ps -> ch)))
2		pm2.43 57	. 2 |- ((ps -> (ps -> ch)) -> (ps -> ch))
3	1, 2	syl 12	1 |- (ph -> (ps -> ch))

Syntax hints:   -> wi 2

This theorem is referenced by:  loolin 66  elimant 505  po2nr 2135  wereu 2197  ordelord 2221  tz7.7 2224  ordtr2 2257  onint 2261  ordsucelsuc 2324  funssres 2698  2elresin 2733  fvopab2 2878  funopfv 2886  isofrlem 2939  tfrlem11 2959  tfr3 2964  tz7.49 2997  nnmass 3181  sbthlem1 3349  mapenlem1 3384  php 3409  pssnn 3428  inf3lem2 3465  r1ord 3499  aceq6b 3565  indpi 3828  genpcd 3903  ltaddpr 3934  ltexprlem7 3942  addcanpr 3946  prlem936 3949  reclem4pr 3953  suplem2pr 3956  suppsr2 4017  sup2 4510  nnunb 4520  uzwo 4605  nnwoOLD 4608  spansncv 5542  pjnormss 5638  sumdmd 5787

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

metamath.org