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

Theorem pm2.43b 55
Description: Inference absorbing redundant antecedent. (Contributed by NM, 31-Oct-1995.)
Hypothesis
Ref Expression
pm2.43b.1 (𝜓 → (𝜑 → (𝜓𝜒)))
Assertion
Ref Expression
pm2.43b (𝜑 → (𝜓𝜒))

Proof of Theorem pm2.43b
StepHypRef Expression
1 pm2.43b.1 . . 3 (𝜓 → (𝜑 → (𝜓𝜒)))
21pm2.43a 54 . 2 (𝜓 → (𝜑𝜒))
32com12 32 1 (𝜑 → (𝜓𝜒))
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  2738  2eu1v  2739  rspcebdv  3603  elpwunsn  4606  trel  5166  preddowncl  6164  predpoirr  6165  predfrirr  6166  funfvima  6986  ordsucss  7529  ac10ct  9460  ltaprlem  10466  infrelb  11624  nnmulcl  11660  ico0  12783  ioc0  12784  clwlkclwwlkfo  27803  n4cyclfrgr  28085  chlimi  29026  atcvatlem  30177  rdgssun  34767  eel12131  41367  lidldomn1  44498
  Copyright terms: Public domain W3C validator