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  2681  2eu1OLD  2682  rspcebdv  3540  elpwunsn  4496  trel  5038  preddowncl  6015  predpoirr  6016  predfrirr  6017  funfvima  6820  ordsucss  7351  ac10ct  9256  ltaprlem  10266  infrelb  11429  nnmulcl  11466  nnmulclOLD  11467  ico0  12603  ioc0  12604  clwlkclwwlkfoOLD  27522  clwlkclwwlkfo  27526  n4cyclfrgr  27828  chlimi  28793  atcvatlem  29946  rdgssun  34101  eel12131  40466  lidldomn1  43557
 Copyright terms: Public domain W3C validator