Theorem pm2.43a 45

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

Syntax hints:   -> wi 4

This theorem is referenced by:  pm2.43b  46  rspc  2878  intss1  3877  fvopab3ig  5599  odi  6577  nndi  6621  inf3lem2  7330  pr2ne  7635  zorn2lem7  8129  uzind2  10104  uzindOLD  10106  sqlecan  11209  clatlem  14216  fiinopn  16647  dvrunz  21100  eqfnung2  25118  supwlub  25274  dfps2  25289  rltrooo  25415  osneisi  25531  limptlimpr2lem1  25574  limptlimpr2lem2  25575  bwt2  25592  icccon4  25702  intvconlem1  25703  propsrc  25868  tartarmap  25888  fnctartar  25907  fnctartar2  25908  domcatfun  25925  indcls2  25996  clscnc  26010  iscol3  26094  isibg1a6  26125  bsstrs  26146  nbssntrs  26147  pdiveql  26168  ee223  28406

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