Theorem pm2.43b 56

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 55	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	com12 33	1 ⊢ (𝜑 → (𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  2eu1  2677  2eu1v  2678  rspcebdv  3574  elpwunsn  4649  trel  5225  preddowncl  6333  predpoirr  6334  predfrirr  6335  funfvima  7228  ordsucss  7812  mapfset  8845  ac10ct  10025  ltaprlem  11035  infrelb  12206  nnmulcl  12263  ico0  13424  ioc0  13425  clwlkclwwlkfo  30371  n4cyclfrgr  30653  chlimi  31597  atcvatlem  32748  rdgssun  38052  eldisjim3  39492  eel12131  45449  lidldomn1  49024