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 1997  intss1 2548  ordsucelsuc 3073  fneu 3592  tz6.12i 3741  fvopab3ig 3778  fvopab2 3791  odi 4210  inf3lem2 4614  rankr1 4674  zorn2lem7 4794  prlem936b 5154  reclem3pr 5158  uzind2 6206  uzindOLD 6208  sqlecant 6641  chcmh 9113  uninqs 10441  fiv 10482  fivOLD 10483  cnvhmphb 10526  homcard 10539  cnfilca 10583  cnfilcaOLD 10584

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

Copyright terms: Public domain