MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43b 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  4243  trss  4245  elpwunsn  4690  ordsucss  4731  funfvima  5905  ac10ct  7841  ltaprlem  8847  nnmulcl  9948  ico0  10887  ioc0  10888  chlimi  22578  atcvatlem  23729  preddowncl  25213  predpoirr  25214  predfrirr  25215  n4cyclfrgra  27764  vdgn0frgrav2  27771  eel12131  28155  eel32131  28158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator