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  2651  2eu1v  2652  rspcebdv  3616  elpwunsn  4684  trel  5268  preddowncl  6353  predpoirr  6354  predfrirr  6355  funfvima  7250  ordsucss  7838  mapfset  8890  ac10ct  10074  ltaprlem  11084  infrelb  12253  nnmulcl  12290  ico0  13433  ioc0  13434  clwlkclwwlkfo  30028  n4cyclfrgr  30310  chlimi  31253  atcvatlem  32404  rdgssun  37379  eel12131  44733  lidldomn1  48147