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

Theorem pm2.43b 52
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 51 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32com12 32 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  2eu1  2359  elpwunsn  3983  trel  4468  trss  4470  preddowncl  5369  predpoirr  5370  predfrirr  5371  funfvima  6099  ordsucss  6603  ac10ct  8416  ltaprlem  9420  infrelb  10547  nnmulcl  10583  ico0  11633  ioc0  11634  clwlkfoclwwlk  25515  n4cyclfrgra  25688  vdgn0frgrav2  25694  chlimi  26829  atcvatlem  27980  eel12131  37013  eel32131  37016  usgvincvad  39317  usgvincvadALT  39320  lidldomn1  39522
  Copyright terms: Public domain W3C validator