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  2641  2eu1v  2642  rspcebdv  3601  elpwunsn  4683  trel  5268  preddowncl  6332  predpoirr  6333  predfrirr  6334  funfvima  7236  ordsucss  7815  mapfset  8860  ac10ct  10049  ltaprlem  11059  infrelb  12221  nnmulcl  12258  ico0  13394  ioc0  13395  clwlkclwwlkfo  29806  n4cyclfrgr  30088  chlimi  31031  atcvatlem  32182  rdgssun  36793  eel12131  44075  lidldomn1  47216