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	|- (-. 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 752  hbae 1145  hbequid 1169  ax17eq 1211  sbequi 1228  sbcom 1258  sbcom2 1334  ax17el 1361  pssnn 4534  axextnd 4943  axunnd 4948  axpowndlem3 4951  axpownd 4953  axregndlem2 4955  axregnd 4956  axinfndlem1 4957  axinfnd 4958  alephadd 7582

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

Copyright terms: Public domain