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  2649  2eu1v  2650  rspcebdv  3616  elpwunsn  4689  trel  5274  preddowncl  6355  predpoirr  6356  predfrirr  6357  funfvima  7250  ordsucss  7838  mapfset  8889  ac10ct  10072  ltaprlem  11082  infrelb  12251  nnmulcl  12288  ico0  13430  ioc0  13431  clwlkclwwlkfo  30038  n4cyclfrgr  30320  chlimi  31263  atcvatlem  32414  rdgssun  37361  eel12131  44711  lidldomn1  48075