MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43a Structured version   Unicode version

Theorem pm2.43a 49
Description: Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by Mel L. 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
StepHypRef Expression
1 id 22 . 2  |-  ( ps 
->  ps )
2 pm2.43a.1 . 2  |-  ( ps 
->  ( ph  ->  ( ps  ->  ch ) ) )
31, 2mpid 41 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  pm2.43b  50  rspc  3190  intss1  4286  fvopab3ig  5938  suppimacnv  6914  odi  7230  nndi  7274  inf3lem2  8049  pr2ne  8386  zorn2lem7  8885  uzind2  10962  uzindOLD  10964  ssfzo12  11887  elfznelfzo  11897  injresinj  11908  suppssfz  12082  sqlecan  12256  brfi1uzind  12514  cramerimplem2  19164  fiinopn  19388  bwthOLD  19889  usgraedg4  24365  wlkdvspthlem  24587  usgrcyclnl1  24618  3cyclfrgrarn1  24990  vdn0frgrav2  25001  vdn1frgrav2  25003  vdgn1frgrav2  25004  numclwlk1lem2foa  25069  dvrunz  25413  afveu  32192  lindslinindsimp2  32934  ee223  33288
  Copyright terms: Public domain W3C validator