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

Theorem pm2.43b 46
Description: Inference absorbing redundant antecedent. (Contributed by NM, 31-Oct-1995.)
Hypothesis
Ref Expression
pm2.43b.1  |-  ( ps 
->  ( ph  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
pm2.43b  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem pm2.43b
StepHypRef Expression
1 pm2.43b.1 . . 3  |-  ( ps 
->  ( ph  ->  ( ps  ->  ch ) ) )
21pm2.43a 45 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32com12 27 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  trel  4136  trss  4138  elpwunsn  4584  ordsucss  4625  funfvima  5769  ac10ct  7677  ltaprlem  8684  nnmulcl  9785  ico0  10718  ioc0  10719  chlimi  21830  atcvatlem  22981  preddowncl  24267  predpoirr  24268  predfrirr  24269  cmptdst  25671  codcatfun  26037  indcls2  26099  pgapspf2  26156  isibg1a2  26220  sgplpte21c  26238  lppotoslem  26246  bsstrs  26249  n4cyclfrgra  28440  eel12131  28798  eel32131  28801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator