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  2648  2eu1v  2649  rspcebdv  3568  elpwunsn  4638  trel  5210  preddowncl  6287  predpoirr  6288  predfrirr  6289  funfvima  7173  ordsucss  7757  mapfset  8783  ac10ct  9935  ltaprlem  10945  infrelb  12117  nnmulcl  12159  ico0  13301  ioc0  13302  clwlkclwwlkfo  30000  n4cyclfrgr  30282  chlimi  31225  atcvatlem  32376  rdgssun  37433  eel12131  44819  lidldomn1  48345