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  2675  2eu1v  2676  rspcebdv  3570  elpwunsn  4644  trel  5219  preddowncl  6324  predpoirr  6325  predfrirr  6326  funfvima  7224  ordsucss  7812  mapfset  8850  ac10ct  10084  ltaprlem  11100  infrelb  12271  nnmulcl  12328  ico0  13491  ioc0  13492  clwlkclwwlkfo  30533  n4cyclfrgr  30825  chlimi  31769  atcvatlem  32920  rdgssun  38221  eldisjim3  39667  eel12131  45639  lidldomn1  49250