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  3556  elpwunsn  4618  trel  5189  preddowncl  6285  predpoirr  6286  predfrirr  6287  funfvima  7174  ordsucss  7758  mapfset  8786  ac10ct  9945  ltaprlem  10956  infrelb  12130  nnmulcl  12187  ico0  13333  ioc0  13334  clwlkclwwlkfo  30067  n4cyclfrgr  30349  chlimi  31293  atcvatlem  32444  rdgssun  37682  eldisjim3  39124  eel12131  45127  lidldomn1  48695