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  2681  2eu1OLD  2682  rspcebdv  3540  elpwunsn  4496  trel  5038  preddowncl  6015  predpoirr  6016  predfrirr  6017  funfvima  6820  ordsucss  7351  ac10ct  9256  ltaprlem  10266  infrelb  11429  nnmulcl  11466  nnmulclOLD  11467  ico0  12603  ioc0  12604  clwlkclwwlkfoOLD  27522  clwlkclwwlkfo  27526  n4cyclfrgr  27828  chlimi  28793  atcvatlem  29946  rdgssun  34101  eel12131  40466  lidldomn1  43557