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:  3imp3i2an  1275  2eu1  2552  elpwunsn  4195  trel  4719  trssOLD  4722  preddowncl  5666  predpoirr  5667  predfrirr  5668  funfvima  6446  ordsucss  6965  ac10ct  8801  ltaprlem  9810  infrelb  10952  nnmulcl  10987  ico0  12163  ioc0  12164  clwlksfoclwwlk  26829  n4cyclfrgr  27019  chlimi  27937  atcvatlem  29090  eel12131  38417  lidldomn1  41206
  Copyright terms: Public domain W3C validator