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

Step	Hyp	Ref	Expression
1		pm2.43b.1	. . 3 ⊢ (𝜓 → (𝜑 → (𝜓 → 𝜒)))
2	1	pm2.43a 54	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	com12 32	1 ⊢ (𝜑 → (𝜓 → 𝜒))

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  2644  2eu1v  2645  rspcebdv  3605  elpwunsn  4686  trel  5273  preddowncl  6332  predpoirr  6333  predfrirr  6334  funfvima  7233  ordsucss  7808  mapfset  8846  ac10ct  10031  ltaprlem  11041  infrelb  12203  nnmulcl  12240  ico0  13374  ioc0  13375  clwlkclwwlkfo  29529  n4cyclfrgr  29811  chlimi  30754  atcvatlem  31905  rdgssun  36562  eel12131  43776  lidldomn1  46911