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  2735  2eu1v  2736  rspcebdv  3619  elpwunsn  4623  trel  5181  preddowncl  6177  predpoirr  6178  predfrirr  6179  funfvima  6994  ordsucss  7535  ac10ct  9462  ltaprlem  10468  infrelb  11628  nnmulcl  11664  ico0  12787  ioc0  12788  clwlkclwwlkfo  27789  n4cyclfrgr  28072  chlimi  29013  atcvatlem  30164  rdgssun  34661  eel12131  41054  lidldomn1  44199