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  2654  2eu1v  2655  rspcebdv  3629  elpwunsn  4707  trel  5292  preddowncl  6364  predpoirr  6365  predfrirr  6366  funfvima  7267  ordsucss  7854  mapfset  8908  ac10ct  10103  ltaprlem  11113  infrelb  12280  nnmulcl  12317  ico0  13453  ioc0  13454  clwlkclwwlkfo  30041  n4cyclfrgr  30323  chlimi  31266  atcvatlem  32417  rdgssun  37344  eel12131  44684  lidldomn1  47954