Theorem pm2.61d2 111

Description: Inference eliminating an antecedent.

Hypotheses

Ref	Expression
pm2.61d2.1	⊢ (φ → (¬ ψ → χ))
pm2.61d2.2	⊢ (ψ → χ)

Assertion

Ref	Expression
pm2.61d2	⊢ (φ → χ)

Proof of Theorem pm2.61d2

Step	Hyp	Ref	Expression
1		pm2.61d2.2	. . 3 ⊢ (ψ → χ)
2	1	a1d 14	. 2 ⊢ (ψ → (φ → χ))
3		pm2.61d2.1	. . 3 ⊢ (φ → (¬ ψ → χ))
4	3	com12 13	. 2 ⊢ (¬ ψ → (φ → χ))
5	2, 4	pm2.61i 110	1 ⊢ (φ → χ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  pm2.61ii 113  tfinds 2401  imasn 2616  ndmoprcl 3058  f1oeng 3298  f1domg 3299  fiint 3445  inf3lemd 3463  axpowndlem3 3745  ltapr 3945  infxpidmlem8 4940  infmap2 4953  pjthlem13 5237  mdsymlem6 5781

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

metamath.org