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