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  2371  elpwunsn  4015  trel  4490  trss  4492  funfvima  6051  ordsucss  6529  ac10ct  8305  ltaprlem  9314  nnmulcl  10446  ico0  11447  ioc0  11448  chlimi  24772  atcvatlem  25924  preddowncl  27791  predpoirr  27792  predfrirr  27793  clwlkfoclwwlk  30656  n4cyclfrgra  30748  vdgn0frgrav2  30755  eel12131  31742  eel32131  31745
  Copyright terms: Public domain W3C validator