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  2645  2eu1v  2646  rspcebdv  3569  elpwunsn  4635  trel  5204  preddowncl  6275  predpoirr  6276  predfrirr  6277  funfvima  7159  ordsucss  7743  mapfset  8769  ac10ct  9917  ltaprlem  10927  infrelb  12099  nnmulcl  12141  ico0  13283  ioc0  13284  clwlkclwwlkfo  29979  n4cyclfrgr  30261  chlimi  31204  atcvatlem  32355  rdgssun  37391  eel12131  44724  lidldomn1  48241