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  2652  2eu1v  2653  rspcebdv  3571  elpwunsn  4642  trel  5214  preddowncl  6291  predpoirr  6292  predfrirr  6293  funfvima  7178  ordsucss  7762  mapfset  8791  ac10ct  9948  ltaprlem  10959  infrelb  12131  nnmulcl  12173  ico0  13311  ioc0  13312  clwlkclwwlkfo  30067  n4cyclfrgr  30349  chlimi  31292  atcvatlem  32443  rdgssun  37554  eldisjim3  38987  eel12131  44989  lidldomn1  48513