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  3573  elpwunsn  4638  trel  5210  preddowncl  6284  predpoirr  6285  predfrirr  6286  funfvima  7170  ordsucss  7757  mapfset  8784  ac10ct  9947  ltaprlem  10957  infrelb  12128  nnmulcl  12170  ico0  13312  ioc0  13313  clwlkclwwlkfo  29971  n4cyclfrgr  30253  chlimi  31196  atcvatlem  32347  rdgssun  37351  eel12131  44686  lidldomn1  48203