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:  3imp3i2anOLD  1300  2eu1  2582  rspcebdv  3345  elpwunsn  4256  trel  4792  trssOLD  4795  preddowncl  5745  predpoirr  5746  predfrirr  5747  funfvima  6532  ordsucss  7060  ac10ct  8895  ltaprlem  9904  infrelb  11046  nnmulcl  11081  ico0  12259  ioc0  12260  clwlksfoclwwlk  27050  n4cyclfrgr  27271  chlimi  28219  atcvatlem  29372  eel12131  39255  lidldomn1  42246
  Copyright terms: Public domain W3C validator