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  3560  elpwunsn  4623  trel  5207  preddowncl  6250  predpoirr  6251  predfrirr  6252  funfvima  7138  ordsucss  7697  mapfset  8669  ac10ct  9840  ltaprlem  10850  infrelb  12010  nnmulcl  12047  ico0  13175  ioc0  13176  clwlkclwwlkfo  28422  n4cyclfrgr  28704  chlimi  29645  atcvatlem  30796  rdgssun  35597  eel12131  42546  lidldomn1  45723