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:  3imp3i2anOLD  1300  2eu1  2582  rspcebdv  3345  elpwunsn  4256  trel  4792  trssOLD  4795  preddowncl  5745  predpoirr  5746  predfrirr  5747  funfvima  6532  ordsucss  7060  ac10ct  8895  ltaprlem  9904  infrelb  11046  nnmulcl  11081  ico0  12259  ioc0  12260  clwlksfoclwwlk  27050  n4cyclfrgr  27271  chlimi  28219  atcvatlem  29372  eel12131  39255  lidldomn1  42246