Propositional Calculus Proofs (5)

Th18) ⊢ P ⇒ (¬P ⇒ Q)
1.) ⊢ ¬P ⇒ (P ⇒ Q)                                            Th17
2.) ⊢  [¬P ⇒ (P ⇒ Q)] ⇒ [P ⇒ (¬P ⇒ Q)]           Th15
3.) ⊢ P ⇒ (¬P ⇒ Q)                                            MP 1,2

Th19) ⊢ ¬¬P ⇒ P
1.) ⊢ ¬¬P ⇒ (¬¬¬¬P ⇒ ¬¬P)                         Lk1
2.) ⊢ [¬(¬¬¬P) ⇒ ¬(¬P)] ⇒ (¬P ⇒ ¬¬¬P)   Lk3
3.) ⊢ [¬P ⇒ ¬(¬¬P)] ⇒ (¬¬P ⇒ P)                Lk3
4.) ⊢ ¬¬P ⇒ (¬¬P ⇒ P)                                   Th8
5.) ⊢ ¬¬P ⇒ P                                                  Th10

Th20) ⊢ Y ⇒ ¬¬Y

1.) ⊢ ¬¬(¬Y) ⇒ (¬Y)                                Th19

2.) ⊢ (¬(¬¬Y) ⇒ ¬Y) ⇒ (Y ⇒ ¬¬Y)         Lk3

3.) ⊢ Y ⇒ ¬¬Y                                           MP 1,2