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  3142  intss1  4227  fvopab3ig  5867  suppimacnv  6846  odi  7164  nndi  7208  inf3lem2  7978  pr2ne  8314  zorn2lem7  8813  uzind2  10890  ssfzo12  11823  elfznelfzo  11833  injresinj  11844  suppssfz  12022  sqlecan  12196  brfi1uzind  12455  cramerimplem2  19290  fiinopn  19514  usgraedg4  24529  wlkdvspthlem  24751  usgrcyclnl1  24782  3cyclfrgrarn1  25154  vdn0frgrav2  25165  vdn1frgrav2  25167  vdgn1frgrav2  25168  numclwlk1lem2foa  25233  dvrunz  25573  afveu  32439  lindslinindsimp2  33299  nn0sumshdiglemB  33476  ee223  33795
  Copyright terms: Public domain W3C validator