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  7179  ordsucss  7763  mapfset  8792  ac10ct  9949  ltaprlem  10960  infrelb  12132  nnmulcl  12174  ico0  13312  ioc0  13313  clwlkclwwlkfo  30089  n4cyclfrgr  30371  chlimi  31314  atcvatlem  32465  rdgssun  37596  eldisjim3  39029  eel12131  45031  lidldomn1  48554