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  2639  2eu1v  2640  rspcebdv  3601  elpwunsn  4688  trel  5274  preddowncl  6338  predpoirr  6339  predfrirr  6340  funfvima  7240  ordsucss  7820  mapfset  8867  ac10ct  10057  ltaprlem  11067  infrelb  12229  nnmulcl  12266  ico0  13402  ioc0  13403  clwlkclwwlkfo  29875  n4cyclfrgr  30157  chlimi  31100  atcvatlem  32251  rdgssun  36927  eel12131  44217  lidldomn1  47405