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

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
StepHypRef Expression
1 id 20 . 2  |-  ( ps 
->  ps )
2 pm2.43a.1 . 2  |-  ( ps 
->  ( ph  ->  ( ps  ->  ch ) ) )
31, 2mpid 39 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator