Theorem pm2.43b 56

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 55	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	com12 33	1 ⊢ (𝜑 → (𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  2eu1  2675  2eu1v  2676  rspcebdv  3570  elpwunsn  4644  trel  5219  preddowncl  6335  predpoirr  6336  predfrirr  6337  funfvima  7236  ordsucss  7829  mapfset  8872  ac10ct  10113  ltaprlem  11129  infrelb  12302  nnmulcl  12359  ico0  13522  ioc0  13523  clwlkclwwlkfo  30600  n4cyclfrgr  30892  chlimi  31836  atcvatlem  32987  rdgssun  38344  eldisjim3  39790  eel12131  45738  lidldomn1  49371