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  2650  2eu1v  2651  rspcebdv  3564  elpwunsn  4632  trel  5219  preddowncl  6272  predpoirr  6273  predfrirr  6274  funfvima  7163  ordsucss  7732  mapfset  8710  ac10ct  9892  ltaprlem  10902  infrelb  12062  nnmulcl  12099  ico0  13227  ioc0  13228  clwlkclwwlkfo  28662  n4cyclfrgr  28944  chlimi  29885  atcvatlem  31036  rdgssun  35705  eel12131  42706  lidldomn1  45897