Theorem
-------
~D | A & B => [J => ~A => [D => ~J]]
Notation
--------
~ = NOT-operator
& = AND-operator
| = OR-operator
=> = IMPLIES-operator
Color Code
----------
Black = statement
Gray = rule used and line reference
Blue = comment
The following proof was developed with the aid of DC Proof 2.0.
Download at http://www.dcproof.com
Proof
-----
Suppose...
1 ~D | A & B
Premise
Prove: J => ~A => [D => ~J]
Suppose...
2 J => ~A
Premise
Prove: D => ~J
Suppose...
3 D
Premise
Convert initial premise to an implication and remove ~~
4 ~~D => A & B
Imply-Or, 1
5 D => A & B
Rem DNeg, 4
Obtain contrapositive rule on 2nd premise and remove ~~
6 ~~A => ~J
Contra, 2
7 A => ~J
Rem DNeg, 6
Apply detachment rule
8 A & B
Detach, 5, 3
9 A
Split, 8
10 B
Split, 8
11 ~J
Detach, 7, 9
As Required:
12 D => ~J
4 Conclusion, 3
As Required:
13 J => ~A => [D => ~J]
4 Conclusion, 2
As Required:
14 ~D | A & B => [J => ~A => [D => ~J]]
4 Conclusion, 1