Theorem pm2.43b 56

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 55	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	com12 33	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  2676  2eu1v  2677  rspcebdv  3574  elpwunsn  4649  trel  5225  preddowncl  6333  predpoirr  6334  predfrirr  6335  funfvima  7228  ordsucss  7813  mapfset  8846  ac10ct  10017  ltaprlem  11028  infrelb  12199  nnmulcl  12256  ico0  13417  ioc0  13418  clwlkclwwlkfo  30326  n4cyclfrgr  30608  chlimi  31552  atcvatlem  32703  rdgssun  37968  eldisjim3  39410  eel12131  45369  lidldomn1  48941