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  2712  2eu1v  2713  rspcebdv  3565  elpwunsn  4581  trel  5143  preddowncl  6143  predpoirr  6144  predfrirr  6145  funfvima  6970  ordsucss  7513  ac10ct  9445  ltaprlem  10455  infrelb  11613  nnmulcl  11649  ico0  12772  ioc0  12773  clwlkclwwlkfo  27794  n4cyclfrgr  28076  chlimi  29017  atcvatlem  30168  rdgssun  34795  eel12131  41419  lidldomn1  44545