BondKing
- 13
- 0
(c v ~ h) - > ~ m (prem 1)
T -> ~ c (prem 2)
T ^ h (prem 3)
trying to get m 1) T (spec prem 3)
2) ~ c ( M.PON prem 2, 1)
3) ~ h (ELIM prem 1 (c v ~ h), 2)
4) ~ h - > ~ m (replace (c v ~ h) with ~h)
5) m -> h (Contrap. 4)
6) ~m v h (M.TOL 5,3)
6) m
T -> ~ c (prem 2)
T ^ h (prem 3)
trying to get m 1) T (spec prem 3)
2) ~ c ( M.PON prem 2, 1)
3) ~ h (ELIM prem 1 (c v ~ h), 2)
4) ~ h - > ~ m (replace (c v ~ h) with ~h)
5) m -> h (Contrap. 4)
6) ~m v h (M.TOL 5,3)
6) m