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

Theorem pm2.43b 50
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 49 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32com12 31 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  2307  elpwunsn  3985  trel  4467  trss  4469  funfvima  6048  ordsucss  6552  ac10ct  8328  ltaprlem  9333  nnmulcl  10475  ico0  11496  ioc0  11497  clwlkfoclwwlk  24966  n4cyclfrgra  25139  vdgn0frgrav2  25145  chlimi  26269  atcvatlem  27420  preddowncl  29441  predpoirr  29442  predfrirr  29443  usgvincvad  32722  usgvincvadALT  32725  lidldomn1  32927  eel12131  33846  eel32131  33849
  Copyright terms: Public domain W3C validator