MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43a 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  2042  rspc  3006  intss1  4025  fvopab3ig  5762  odi  6781  nndi  6825  inf3lem2  7540  pr2ne  7845  zorn2lem7  8338  uzind2  10318  uzindOLD  10320  elfznelfzo  11147  injresinj  11155  sqlecan  11442  brfi1uzind  11670  clatlem  14494  fiinopn  16929  usgraedg4  21359  wlkdvspthlem  21560  usgrcyclnl1  21580  dvrunz  21974  afveu  27884  ssfzo12  27990  swrdccatin12lem3c  28023  3cyclfrgrarn1  28116  vdn0frgrav2  28128  vdn1frgrav2  28130  vdgn1frgrav2  28131  ee223  28444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator