Theorem pm2.43b 61

Description: Inference absorbing redundant antecedent.

Hypothesis

Ref	Expression
pm2.43a.1	⊢ (ψ → (φ → (ψ → χ)))

Assertion

Ref	Expression
pm2.43b	⊢ (φ → (ψ → χ))

Proof of Theorem pm2.43b

Step	Hyp	Ref	Expression
1		pm2.43a.1	. . 3 ⊢ (ψ → (φ → (ψ → χ)))
2	1	pm2.43a 60	. 2 ⊢ (ψ → (φ → χ))
3	2	com12 13	1 ⊢ (φ → (ψ → χ))

Syntax hints:   → wi 2

This theorem is referenced by:  anabsi7 379  rcla4v 1402  elinti 1974  trel 2048  trss 2050  onfr 2237  ordsucss 2320  limom 2387  vtoclr 2449  ralxp 2456  fvelima 2859  funfvima 2904  nnmordi 3188  ensymg 3316  domsdomtr 3374  ltaprlem 3944  nnmulclt 4437  crulem 4528  chlim 5139  atcvatlem 5770

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org