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