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  2735  2eu1v  2736  rspcebdv  3617  elpwunsn  4621  trel  5179  preddowncl  6175  predpoirr  6176  predfrirr  6177  funfvima  6992  ordsucss  7533  ac10ct  9460  ltaprlem  10466  infrelb  11626  nnmulcl  11662  ico0  12785  ioc0  12786  clwlkclwwlkfo  27787  n4cyclfrgr  28070  chlimi  29011  atcvatlem  30162  rdgssun  34662  eel12131  41067  lidldomn1  44212