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

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
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
2 pm2.43a.1 . 2  |-  ( ps 
->  ( ph  ->  ( ps  ->  ch ) ) )
31, 2mpid 37 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  pm2.43b  46  rspc  2963  intss1  3979  fvopab3ig  5706  odi  6719  nndi  6763  inf3lem2  7477  pr2ne  7782  zorn2lem7  8276  uzind2  10255  uzindOLD  10257  elfznelfzo  11079  injresinj  11087  sqlecan  11374  brfi1uzind  11602  clatlem  14426  fiinopn  16864  usgraedg4  21083  dvrunz  21411  afveu  27524  wlkdvspthlem  27745  usgrcyclnl1  27766  3cyclfrgrarn1  27847  vdn0frgrav2  27859  vdn1frgrav2  27861  vdgn1frgrav2  27862  ee223  28159
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator