Theorem pm2.43b 55

Description: Inference absorbing redundant antecedent. (Contributed by NM, 31-Oct-1995.)

Hypothesis

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

Assertion

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

Proof of Theorem pm2.43b

Step	Hyp	Ref	Expression
1		pm2.43b.1	. . 3 |- ( ps -> ( ph -> ( ps -> ch ) ) )
2	1	pm2.43a 54	. 2 |- ( ps -> ( ph -> ch ) )
3	2	com12 32	1 |- ( ph -> ( ps -> ch ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  3imp3i2an  1278  2eu1  2553  rspcebdv  3314  elpwunsn  4224  trel  4759  trssOLD  4762  preddowncl  5707  predpoirr  5708  predfrirr  5709  funfvima  6492  ordsucss  7018  ac10ct  8857  ltaprlem  9866  infrelb  11008  nnmulcl  11043  ico0  12221  ioc0  12222  clwlksfoclwwlk  26963  n4cyclfrgr  27155  chlimi  28091  atcvatlem  29244  eel12131  38938  lidldomn1  41921