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  2640  2eu1v  2641  rspcebdv  3602  elpwunsn  4692  trel  5279  preddowncl  6345  predpoirr  6346  predfrirr  6347  funfvima  7247  ordsucss  7827  mapfset  8879  ac10ct  10077  ltaprlem  11087  infrelb  12251  nnmulcl  12288  ico0  13424  ioc0  13425  clwlkclwwlkfo  29942  n4cyclfrgr  30224  chlimi  31167  atcvatlem  32318  rdgssun  37085  eel12131  44389  lidldomn1  47608