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  2085  rspc  3046  intss1  4065  fvopab3ig  5803  odi  6822  nndi  6866  inf3lem2  7584  pr2ne  7889  zorn2lem7  8382  uzind2  10362  uzindOLD  10364  elfznelfzo  11192  injresinj  11200  sqlecan  11487  brfi1uzind  11715  clatlem  14539  fiinopn  16974  bwth  17473  usgraedg4  21406  wlkdvspthlem  21607  usgrcyclnl1  21627  dvrunz  22021  afveu  27993  ssfzo12  28130  3cyclfrgrarn1  28402  vdn0frgrav2  28414  vdn1frgrav2  28416  vdgn1frgrav2  28417  ee223  28735

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