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  3582  elpwunsn  4648  trel  5223  preddowncl  6305  predpoirr  6306  predfrirr  6307  funfvima  7204  ordsucss  7793  mapfset  8823  ac10ct  9987  ltaprlem  10997  infrelb  12168  nnmulcl  12210  ico0  13352  ioc0  13353  clwlkclwwlkfo  29938  n4cyclfrgr  30220  chlimi  31163  atcvatlem  32314  rdgssun  37366  eel12131  44702  lidldomn1  48219