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  2652  2eu1v  2653  rspcebdv  3559  elpwunsn  4629  trel  5201  preddowncl  6288  predpoirr  6289  predfrirr  6290  funfvima  7176  ordsucss  7760  mapfset  8788  ac10ct  9945  ltaprlem  10956  infrelb  12128  nnmulcl  12170  ico0  13308  ioc0  13309  clwlkclwwlkfo  30068  n4cyclfrgr  30350  chlimi  31294  atcvatlem  32445  rdgssun  37690  eldisjim3  39127  eel12131  45142  lidldomn1  48665