THEOREM

*******

P => [Q => P]

PROOF

*****

Suppose to the contrary...

1 ~[P => [Q => P]]

Premise

Apply Imply-And Rule for both '=>' (previously justified here)

2 ~~[P & ~[Q => P]]

Imply-And, 1

3 ~~[P & ~~[Q & ~P]]

Imply-And, 2

Remove each ~~

4 P & ~~[Q & ~P]

Rem DNeg, 3

5 P & [Q & ~P]

Rem DNeg, 4

Apply Split Rule

6 P

Split, 5

7 Q & ~P

Split, 5

8 Q

Split, 7

9 ~P

Split, 7

Obtain contradiction...

10 P & ~P

Join, 6, 9

Apply Conclusion Rule (Proof by contradiction)

11 ~~[P => [Q => P]]

4 Conclusion, 1

Remove ~~

12 P => [Q => P]

Rem DNeg, 11