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  2652  2eu1v  2653  rspcebdv  3559  elpwunsn  4629  trel  5201  preddowncl  6297  predpoirr  6298  predfrirr  6299  funfvima  7185  ordsucss  7769  mapfset  8797  ac10ct  9956  ltaprlem  10967  infrelb  12141  nnmulcl  12198  ico0  13344  ioc0  13345  clwlkclwwlkfo  30079  n4cyclfrgr  30361  chlimi  31305  atcvatlem  32456  rdgssun  37694  eldisjim3  39136  eel12131  45139  lidldomn1  48701