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  2645  2eu1v  2646  rspcebdv  3585  elpwunsn  4651  trel  5226  preddowncl  6308  predpoirr  6309  predfrirr  6310  funfvima  7207  ordsucss  7796  mapfset  8826  ac10ct  9994  ltaprlem  11004  infrelb  12175  nnmulcl  12217  ico0  13359  ioc0  13360  clwlkclwwlkfo  29945  n4cyclfrgr  30227  chlimi  31170  atcvatlem  32321  rdgssun  37373  eel12131  44709  lidldomn1  48223