Theorem pm2.43a 66

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

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 1993  intss1 2543  ordsucelsuc 3068  fneu 3584  tz6.12i 3732  fvopab3ig 3769  fvopab2 3782  odi 4200  inf3lem2 4594  rankr1 4654  zorn2lem7 4774  prlem936b 5134  reclem3pr 5138  uzind2 6162  uzindOLD 6164  sqlecant 6580  chcmh 9052  uninqs 10378  fiv 10410  cnvhmphb 10449  homcard 10462  cnfilca 10487

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

Copyright terms: Public domain