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  2653  2eu1v  2654  rspcebdv  3553  elpwunsn  4624  trel  5202  preddowncl  6232  predpoirr  6233  predfrirr  6234  funfvima  7100  ordsucss  7653  mapfset  8612  ac10ct  9774  ltaprlem  10784  infrelb  11943  nnmulcl  11980  ico0  13107  ioc0  13108  clwlkclwwlkfo  28352  n4cyclfrgr  28634  chlimi  29575  atcvatlem  30726  rdgssun  35528  eel12131  42286  lidldomn1  45431