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  3573  elpwunsn  4648  trel  5224  preddowncl  6334  predpoirr  6335  predfrirr  6336  funfvima  7232  ordsucss  7817  mapfset  8854  ac10ct  10040  ltaprlem  11056  infrelb  12227  nnmulcl  12284  ico0  13446  ioc0  13447  clwlkclwwlkfo  30465  n4cyclfrgr  30757  chlimi  31701  atcvatlem  32852  rdgssun  38119  eldisjim3  39550  eel12131  45522  lidldomn1  49133