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  2678  2eu1v  2679  rspcebdv  3576  elpwunsn  4644  trel  5216  preddowncl  6319  predpoirr  6320  predfrirr  6321  funfvima  7214  ordsucss  7798  mapfset  8831  ac10ct  10002  ltaprlem  11013  infrelb  12187  nnmulcl  12244  ico0  13405  ioc0  13406  clwlkclwwlkfo  30218  n4cyclfrgr  30500  chlimi  31444  atcvatlem  32595  rdgssun  37877  eldisjim3  39319  eel12131  45279  lidldomn1  48844