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

Theorem pm2.43b 48
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 47 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32com12 29 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  trel  4302  trss  4304  elpwunsn  4750  ordsucss  4791  funfvima  5966  ac10ct  7908  ltaprlem  8914  nnmulcl  10016  ico0  10955  ioc0  10956  chlimi  22730  atcvatlem  23881  preddowncl  25464  predpoirr  25465  predfrirr  25466  n4cyclfrgra  28346  vdgn0frgrav2  28353  eel12131  28759  eel32131  28762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator