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  4120  trss  4122  elpwunsn  4568  ordsucss  4609  funfvima  5753  ac10ct  7661  ltaprlem  8668  nnmulcl  9769  ico0  10702  ioc0  10703  chlimi  21814  atcvatlem  22965  preddowncl  24196  predpoirr  24197  predfrirr  24198  cmptdst  25568  codcatfun  25934  indcls2  25996  pgapspf2  26053  isibg1a2  26117  sgplpte21c  26135  lppotoslem  26143  bsstrs  26146
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator