Theorem pm2.43a 66

Description: Inference absorbing redundant antecedent. (The proof was shortened by O'Cat, 3-Feb-06.)

Hypothesis

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

Assertion

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

Proof of Theorem pm2.43a

Step	Hyp	Ref	Expression
1		ax-1 4	. 2 |- (ps -> (ph -> ps))
2		pm2.43a.1	. 2 |- (ps -> (ph -> (ps -> ch)))
3	1, 2	mpdd 46	1 |- (ps -> (ph -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.43b 67  ra4sbc 1987  intss1 2538  ordsucelsuc 3063  fneu 3578  tz6.12i 3726  fvopab3ig 3763  fvopab2 3776  odi 4194  inf3lem2 4586  rankr1 4646  zorn2lem7 4766  prlem936b 5126  reclem3pr 5130  uzind2 6154  uzindOLD 6156  sqlecant 6572  chcmh 9034  uninqs 10342  fiv 10374  cnvhmphb 10413  homcard 10426  cnfilca 10451

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain