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  4269  trss  4271  elpwunsn  4716  ordsucss  4757  funfvima  5932  ac10ct  7871  ltaprlem  8877  nnmulcl  9979  ico0  10918  ioc0  10919  chlimi  22690  atcvatlem  23841  preddowncl  25410  predpoirr  25411  predfrirr  25412  n4cyclfrgra  28122  vdgn0frgrav2  28129  eel12131  28530  eel32131  28533
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator