Theorem pm2.61ii 130

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

Hypotheses

Ref	Expression
pm2.61ii.1	|- (-. ph -> (-. ps -> ch))
pm2.61ii.2	|- (ph -> ch)
pm2.61ii.3	|- (ps -> ch)

Assertion

Ref	Expression
pm2.61ii	|- ch

Proof of Theorem pm2.61ii

Step	Hyp	Ref	Expression
1		pm2.61ii.2	. 2 |- (ph -> ch)
2		pm2.61ii.1	. . 3 |- (-. ph -> (-. ps -> ch))
3		pm2.61ii.3	. . 3 |- (ps -> ch)
4	2, 3	pm2.61d2 129	. 2 |- (-. ph -> ch)
5	1, 4	pm2.61i 126	1 |- ch

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.61iii 132  ecase3 749  hbae 1128  ax17eq 1195  ax17el 1196  sbequi 1212  sbcom 1242  sbcom2 1316  pssnn 4465  axextnd 4866  axunnd 4871  axpowndlem3 4874  axpownd 4876  axregndlem2 4878  axregnd 4879  axinfndlem1 4880  axinfnd 4881  alephadd 7475

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

Copyright terms: Public domain