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

Theorem pm2.43b 53
 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 52 . 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  1270  2eu1  2541  elpwunsn  4171  trel  4687  trssOLD  4690  preddowncl  5624  predpoirr  5625  predfrirr  5626  funfvima  6396  ordsucss  6910  ac10ct  8740  ltaprlem  9745  infrelb  10885  nnmulcl  10920  ico0  12092  ioc0  12093  clwlkfoclwwlk  26372  n4cyclfrgra  26545  vdgn0frgrav2  26551  chlimi  27475  atcvatlem  28628  eel12131  37959  clwlksfoclwwlk  41270  n4cyclfrgr  41461  lidldomn1  41711
 Copyright terms: Public domain W3C validator