Theorem pm2.43a 47

Description: Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by O'Cat, 28-Nov-2008.)

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		id 20	. 2 |- ( ps -> ps )
2		pm2.43a.1	. 2 |- ( ps -> ( ph -> ( ps -> ch ) ) )
3	1, 2	mpid 39	1 |- ( ps -> ( ph -> ch ) )

Syntax hints:   -> wi 4

This theorem is referenced by:  pm2.43b  48  equveli  2042  rspc  3006  intss1  4025  fvopab3ig  5762  odi  6781  nndi  6825  inf3lem2  7540  pr2ne  7845  zorn2lem7  8338  uzind2  10318  uzindOLD  10320  elfznelfzo  11147  injresinj  11155  sqlecan  11442  brfi1uzind  11670  clatlem  14494  fiinopn  16929  usgraedg4  21359  wlkdvspthlem  21560  usgrcyclnl1  21580  dvrunz  21974  afveu  27884  ssfzo12  27990  swrdccatin12lem3c  28023  3cyclfrgrarn1  28116  vdn0frgrav2  28128  vdn1frgrav2  28130  vdgn1frgrav2  28131  ee223  28444

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