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  2667  2eu1v  2668  rspcebdv  3566  elpwunsn  4633  trel  5205  preddowncl  6304  predpoirr  6305  predfrirr  6306  funfvima  7199  ordsucss  7783  mapfset  8816  ac10ct  9976  ltaprlem  10988  infrelb  12163  nnmulcl  12220  ico0  13381  ioc0  13382  clwlkclwwlkfo  30146  n4cyclfrgr  30428  chlimi  31372  atcvatlem  32523  rdgssun  37810  eldisjim3  39252  eel12131  45226  lidldomn1  48791