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  2678  2eu1v  2679  rspcebdv  3574  elpwunsn  4645  trel  5223  preddowncl  6353  predpoirr  6354  predfrirr  6355  funfvima  7259  ordsucss  7853  mapfset  8900  ac10ct  10140  ltaprlem  11156  infrelb  12329  nnmulcl  12386  ico0  13549  ioc0  13550  clwlkclwwlkfo  30630  n4cyclfrgr  30922  chlimi  31866  atcvatlem  33017  rdgssun  38493  eldisjim3  39939  eel12131  45886  lidldomn1  49533