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  2647  2eu1v  2648  rspcebdv  3607  elpwunsn  4688  trel  5275  preddowncl  6334  predpoirr  6335  predfrirr  6336  funfvima  7232  ordsucss  7806  mapfset  8844  ac10ct  10029  ltaprlem  11039  infrelb  12199  nnmulcl  12236  ico0  13370  ioc0  13371  clwlkclwwlkfo  29262  n4cyclfrgr  29544  chlimi  30487  atcvatlem  31638  rdgssun  36259  eel12131  43474  lidldomn1  46823