Propositional Calculus Proofs (7)

Th25) ⊢ (B ⇒ ¬B) ⇒ ¬B
1.) ⊢ (B ⇒ ¬B) ⇒ [¬(¬B) ⇒ ¬B]                            Th24
2.) ⊢ ¬(¬B) ⇒ [¬B ⇒ ¬(B ⇒ B)]                            Th17
3.) ⊢ [¬(¬B) ⇒ ¬B] ⇒ [¬(¬B) ⇒ ¬(B ⇒ B)]         Th2
4.)  [¬(¬B) ⇒ ¬(B ⇒ B)] ⇒ [(B ⇒ B) ⇒ (¬B)]   Lk3
5.) ⊢ (B ⇒ ¬B) ⇒ [(B ⇒ B) ⇒ (¬B)]                      Th8
6.) ⊢ B ⇒ B                                                              Th3
7.) ⊢ (B ⇒ ¬B) ⇒ ¬B                                               Th6

Th26) ⊢ (P ⇒ Q) ⇒ [(P ⇒ ¬Q) ⇒ ¬P]
1.) ⊢ (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)                                                                         Th24
2.) ⊢ P ⇒ [(P ⇒ Q) ⇒ (¬Q ⇒ ¬P)]                                                              Th1
3.) ⊢ {P ⇒ [(P ⇒ Q) ⇒ (¬Q ⇒ ¬P)]} ⇒ {(P ⇒ Q) ⇒ [P ⇒ (¬Q ⇒ ¬P)]}   Th15
4.) ⊢ (P ⇒ Q) ⇒ [P ⇒ (¬Q ⇒ ¬P)]                                                              MP 2,3
5.)  [P ⇒ (¬Q ⇒ ¬P)] ⇒ [(P ⇒ ¬Q) ⇒ (P ⇒ ¬P)]                                    Lk2
6.) ⊢ (P ⇒ Q) ⇒ [(P ⇒ ¬Q) ⇒ (P ⇒ ¬P)]                                                   Th5
7.) ⊢ (P ⇒ ¬P) ⇒ ¬P                                                                                    Th25
8.) ⊢ (P ⇒ Q) ⇒ [(P ⇒ ¬Q) ⇒ ¬P]                                                              Th14