Theorem pm2.61nii 131

Description: Inference eliminating two antecedents.

Hypotheses

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

Assertion

Ref	Expression
pm2.61nii	⊢ χ

Proof of Theorem pm2.61nii

Step	Hyp	Ref	Expression
1		pm2.61nii.1	. . . 4 ⊢ (φ → (ψ → χ))
2	1	com12 11	. . 3 ⊢ (ψ → (φ → χ))
3		pm2.61nii.2	. . 3 ⊢ (¬ φ → χ)
4	2, 3	pm2.61d1 128	. 2 ⊢ (ψ → χ)
5		pm2.61nii.3	. 2 ⊢ (¬ ψ → χ)
6	4, 5	pm2.61i 126	1 ⊢ χ

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  ecase 752  3ecase 921  prex 2776

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

Copyright terms: Public domain