Theorem pm2.61ii 130

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

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 129	. 2 ⊢ (¬ φ → χ)
5	1, 4	pm2.61i 126	1 ⊢ χ

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  pm2.61iii 132  ecase3 751  hbae 1143  ax17eq 1209  sbequi 1226  sbcom 1256  sbcom2 1332  ax17el 1359  pssnn 4519  axextnd 4923  axunnd 4928  axpowndlem3 4931  axpownd 4933  axregndlem2 4935  axregnd 4936  axinfndlem1 4937  axinfnd 4938  alephadd 7532

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

Copyright terms: Public domain