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

Theorem pm2.43b 51
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 50 . 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:  3imp3i2an  1244  2eu1  2402  elpwunsn  4003  trel  4497  trss  4499  preddowncl  5414  predpoirr  5415  predfrirr  5416  funfvima  6157  ordsucss  6664  ac10ct  8483  ltaprlem  9487  infrelb  10618  nnmulcl  10654  ico0  11707  ioc0  11708  clwlkfoclwwlk  25652  n4cyclfrgra  25825  vdgn0frgrav2  25831  chlimi  26968  atcvatlem  28119  eel12131  37161  usgvincvad  40224  usgvincvadALT  40227  lidldomn1  40429
  Copyright terms: Public domain W3C validator