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  2650  2eu1v  2651  rspcebdv  3595  elpwunsn  4660  trel  5238  preddowncl  6321  predpoirr  6322  predfrirr  6323  funfvima  7222  ordsucss  7812  mapfset  8864  ac10ct  10048  ltaprlem  11058  infrelb  12227  nnmulcl  12264  ico0  13408  ioc0  13409  clwlkclwwlkfo  29990  n4cyclfrgr  30272  chlimi  31215  atcvatlem  32366  rdgssun  37396  eel12131  44737  lidldomn1  48206