Theorem pm2.61ii 113

Description: Inference eliminating two antecedents. (The proof was shortened by Josh Purinton, 29-Dec-00.)

Hypotheses

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

Assertion

Ref	Expression
pm2.61ii	⊢ χ

Proof of Theorem pm2.61ii

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

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  pm2.61iii 114  ecase3 559  eq5 824  sbequi 876  sbcom 916  ax17eq 923  ax17el 924  sbcom2 992  pssnn 3428  axextnd 3737  axunnd 3742  axpowndlem3 3745  axpownd 3747  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axinfnd 3752

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

metamath.org