4.1
P .: P
1.  SHOW: P
2.    P                       :PR
3.  :DD 2

4.2
P, (P->(P->Q)) .: Q
1.  SHOW: Q
2.    P                       :PR
3.    P->(P->Q)               :PR
4.    P->Q                    :MP 2 3
5.    Q                       :MP 2 4
6.  :DD 5

4.3
P, Q, (P->(Q->R)) .: R
1.  SHOW: R
2.    P                       :PR
3.    Q                       :PR
4.    P->(Q->R)               :PR
5.    Q->R                    :MP 2 4
6.    R                       :MP 3 5
7.  :DD 6

4.4
~P, (~Q->P) .: Q
1.  SHOW: Q
2.    ~P                      :PR
3.    ~Q->P                   :PR
4.    ~~Q                     :MT 2 3
5.    Q                       :DNE 4
6.  :DD 5

4.5
P, (~Q->~P) .: Q
1.  SHOW: Q
2.    P                       :PR
3.    ~Q->~P                  :PR
4.    ~~P                     :DNI 2
5.    ~~Q                     :MT 3 4
6.    Q                       :DNE 5
7.  :DD 6

5.1
T .: (P->P)
1.  SHOW: P->P
2.    P                       :AS
3.  :CD 2

5.2
Q .: (P->Q)
1.  SHOW: P->Q
2.    P                       :AS
3.    Q                       :PR
4.  :CD 3

5.3
P .: ((P->Q)->Q)
1.  SHOW: (P->Q)->Q
2.    P->Q                    :AS
3.    P                       :PR
4.    Q                       :MP 2 3
5.  :CD 4

5.4
(P->Q), (Q->R) .: (P->R)
1.  SHOW: P->R
2.    P                       :AS
3.    P->Q                    :PR
4.    Q->R                    :PR
5.    Q                       :MP 2 3
6.    R                       :MP 4 5
7.  :CD 6

5.5
(P->(P->Q)) .: (P->Q)
1.  SHOW: P->Q
2.    P                       :AS
3.    P->(P->Q)               :PR
4.    P->Q                    :MP 2 3
5.    Q                       :MP 2 4
6.  :CD 5

5.6
T .: (~~P->P)
1.  SHOW: ~~P->P
2.    ~~P                     :AS
3.    P                       :DNE 2
4.   :CD 3

5.7
(P->Q) .: (~Q->~P)
1.  SHOW: ~Q->~P
2.    ~Q                      :AS
3.    P->Q                    :PR
4.    ~P                      :MT 2 3
5.  :CD 4

5.8
(~Q->~P) .: (P->Q)
1.  SHOW: P->Q
2.    P                       :AS
3.    ~Q->~P                  :PR
4.    ~~P                     :DNI 2
5.    ~~Q                     :MT 3 4
6.    Q                       :DNE 5
7.  :CD 6

5.9
(Q->P) .: (~~Q->P)
1.  SHOW: ~~Q->P
2.    ~~Q                     :AS
3.    Q->P                    :PR
4.    Q                       :DNE 2
5.    P                       :MP 3 4
6.  :CD 5

5.10
(P->~Q), (R->Q) .: (P->~R)
1.  SHOW: P->~R
2.    P                       :AS
3.    P->~Q                   :PR
4.    R->Q                    :PR
5.    ~Q                      :MP 2 3
6.    ~R                      :MT 4 5
7.  :CD 6

6.1
T .: (P->(Q->P))
1.  SHOW: P->(Q->P)
2.    P                       :AS
3.    SHOW: Q->P
4.      Q                     :AS
5.    :CD 2
6.  :CD 3

6.2
(P->Q) .: ((Q->R)->(P->R))
1.  SHOW: (Q->R)->(P->R)
2.    Q->R                    :AS
3.    SHOW: P->R
4.      P                     :AS
5.      P->Q                  :PR
6.      Q                     :MP 4 5
7.      R                     :MP 2 6
8.    :CD 7
9.  :CD 3

6.3
(P->(Q->R)) .: ((P->Q)->(P->R))
1.  SHOW: (P->Q)->(P->R)
2.    P->Q                    :AS
3.    SHOW: P->R
4.      P                     :AS
5.      P->(Q->R)             :PR
6.      Q->R                  :MP 4 5
7.      Q                     :MP 2 4
8.      R                     :MP 6 7
9.    :CD 8
10. :CD 3

6.4
(P->(Q->R)) .: (Q->(P->R))
1.  SHOW: Q->(P->R)
2.    Q                       :AS
3.    SHOW: P->R
4.      P                     :AS
5.      P->(Q->R)             :PR
6.      Q->R                  :MP 4 5
7.      R                     :MP 2 6
8.    :CD 7
9.  :CD 3

6.5
((S->R)->Q), R .: Q
1.  SHOW: Q
2.    (S->R)->Q               :PR
3.    SHOW: S->R
4.      S                     :AS
5.      R                     :PR
6.    :CD 5
7.    Q                       :MP 2 3
8.  :DD 7

7.1
(~P->P) .: ~~P
1.  SHOW: ~~P
2.    ~P                      :AS
3.    ~P->P                   :PR
4.    ~~P                     :MT 2 3
5.    P                       :DNE 4
6.  :ID 2 5

7.2
P, ~P .: ~Q
1.  SHOW: ~Q
2.    Q                       :AS
3.    P                       :PR
4.    ~P                      :PR
5.  :ID 3 4

7.3
(~Q->R), (S->~R), (~S->Q) .: ~~Q
1.  SHOW: ~~Q
2.    ~Q                      :AS
3.    ~Q->R                   :PR
4.    S->~R                   :PR
5.    ~S->Q                   :PR
6.    R                       :MP 2 3
7.    ~~R                     :DNI 6
8.    ~S                      :MT 4 7
9.    Q                       :MP 5 8
10.   ~~Q                     :DNI 9
11. :ID 2 10

7.4
(P->Q), (Q->R), (R->S), P .: ~(P->~S)
1.  SHOW: ~(P->~S)
2.    P->~S                   :AS
3.    P->Q                    :PR
4.    Q->R                    :PR
5.    R->S                    :PR
6.    P                       :PR
7.    ~S                      :MP 2 6
8.    Q                       :MP 3 6
9.    R                       :MP 4 8
10.   S                       :MP 5 9
11. :ID 7 10

7.5
((P->Q)->R), (S->(P->Q)), (~S->R) .: ~~R
1.  SHOW: ~~R
2.    ~R                      :AS
3.    (P->Q)->R               :PR
4.    S->(P->Q)               :PR
5.    ~S->R                   :PR
6.    ~(P->Q)                 :MT 2 3
7.    ~~S                     :MT 2 5
8.    S                       :DNE 7
9.    P->Q                    :MP 4 8
10. :ID 6 9

7.6
(~P->(R->S)), ((R->S)->T), ~T, (Q->(R->S)) .: ~(P->Q)
1.  SHOW: ~(P->Q)
2.    P->Q                    :AS
3.    ~P->(R->S)              :PR
4.    (R->S)->T               :PR
5.    ~T                      :PR
6.    Q->(R->S)               :PR
7.    ~(R->S)                 :MT 4 5
8.    ~~P                     :MT 3 7
9.    P                       :DNE 8
10.   Q                       :MP 2 9
11.   R->S                    :MP 6 10
12. :ID 7 11

7.7
T .: ((~P->P)->~~P)
1.  SHOW: (~P->P)->~~P
2.    ~P->P                   :AS
3.    SHOW: ~~P
4.      ~P                    :AS
5.      P                     :MP 2 4
6.    :ID 4 5
7.  :CD 3

7.8
(R->(Q->P)), (Q->~P) .: (R->~Q)
1.  SHOW: R->~Q
2.    R                       :AS
3.    SHOW: ~Q
4.      Q                     :AS
5.      R->(Q->P)             :PR
6.      Q->~P                 :PR
7.      Q->P                  :MP 2 5
8.      ~P                    :MP 4 6
9.      P                     :MP 4 7
10.   :ID 8 9
11. :CD 3

7.9
(P->Q), (Q->R), (R->S) .: (P->~(P->~S))
1.  SHOW: P->~(P->~S)
2.    P                       :AS
3.    SHOW: ~(P->~S)
4.      P->~S                 :AS
5.      P->Q                  :PR
6.      Q->R                  :PR
7.      R->S                  :PR
8.      ~S                    :MP 2 4
9.      ~R                    :MT 7 8
10.     ~Q                    :MT 6 9
11.     ~P                    :MT 5 10
12.   :ID 2 11
13. :CD 3

7.10
(P->Q), ((R->Q)->~P) .: ~P
1.  SHOW: ~P
2.    P                       :AS
3.    P->Q                    :PR
4.    (R->Q)->~P              :PR
5.    SHOW: R->Q
6.      R                     :AS
7.      Q                     :MP 2 3
8.    :CD 7
9.    ~P                      :MP 4 5
10. :ID 2 9

8.1
(P->Q), (Q->R), ((P->R)->(U->S)), (S->T) .: (U->T)
1.  SHOW: U->T
2.    U                       :AS
3.    SHOW: P->R
4.      P                     :AS
5.      P->Q                  :PR
6.      Q                     :MP 4 5
7.      Q->R                  :PR
8.      R                     :MP 6 7
9.    :CD 8
10.   (P->R)->(U->S)          :PR
11.   U->S                    :MP 3 10
12.   S                       :MP 2 11
13.   S->T                    :PR
14.   T                       :MP 12 13
15. :CD 14

8.2
(P->(P->R)), ((P->R)->R) .: R
1.  SHOW: R
2.    (P->R)->R               :PR
3.    SHOW: P->R
4.      P                     :AS
5.      P->(P->R)             :PR
6.      P->R                  :MP 4 5
7.      R                     :MP 4 6
8.    :CD 7
9.    R                       :MP 2 3
10. :DD 9

8.3
T, ((R->T)->~Q), ((Q->S)->W) .: W
1.  SHOW: W
2.   SHOW:R->T
3.    R                       :AS
4.    T                       :PR
5.   :CD 4
6.   (R->T)->~Q               :PR
7.   ~Q                       :MP 2 6
8.   SHOW: Q->S
9.    Q                       :AS
10.   S                       :EFQ 7 9
11.  :CD 10
12.  (Q->S)->W                :PR
13.  W                        :MP 8 12
14. :DD 13

8.4
(P->~(S->W)), W .: (P->(Q->R))
1.  SHOW: P->(Q->R)
2.    P                       :AS
3.    P->~(S->W)              :PR
4.    ~(S->W)                 :MP 2 3
5.    S/\~W                   :NCND_1 4
6.    ~W                      :S 5
7.    W                       :PR
8.    Q->R                    :EFQ 6 7
9.  :CD 8

8.5
T .: (S->((~P->~Q)->(Q->P)))
1.  SHOW: S->((~P->~Q)->(Q->P))
2.   S                        :AS
3.   SHOW: (~P->~Q)->(Q->P)
4.    ~P->~Q                  :AS
5.    SHOW: Q->P
6.     Q                      :AS
7.     ~~Q                    :DNI 6
8.     ~~P                    :MT 4 7
9.     P                      :DNE 8
10.   :CD 9
11.  :CD 5
12. :CD 3

8.6
((R->S)->~P), (Q->T), (~Q->(R->S)), (T->(U->V)) .: (P->(~V->~U))
1.  SHOW: P->(~V->~U)
2.    P                       :AS
3.    ~Q->(R->S)              :PR
4.    (R->S)->~P              :PR
5.    Q->T                    :PR
6.    T->(U->V)               :PR
7.    ~Q->~P                  :HS 3 4
8.    Q->(U->V)               :HS 5 6
9.    P->Q                    :CONP_2 7
10.   P->(U->V)               :HS 8 9
11.   U->V                    :MP 2 10
12.   ~V->~U                  :CONP_1 11
13. :CD 12

8.7
(P->R), (R->~Q), (S->P), (Q->S) .: ~Q
1.  SHOW: ~Q
2.   P->R                     :PR
3.   R->~Q                    :PR
4.   S->P                     :PR
5.   Q->S                     :PR
6.   Q->P                     :HS 4 5
7.   P->~Q                    :HS 2 3
8.   ~P->~Q                   :CONP_1 6
9.   ~Q                       :DIL 7 8
10. :DD 9

8.8
(~Q->~~P), (~~R->~Q), (~R->P) .: P
1.  SHOW: P
2.    ~R->P                   :PR
3.    ~~R->~Q                 :PR
4.    ~Q->~~P                 :PR
5.    ~~R->~~P                :HS 3 4
6.    ~P->~R                  :CONP_2 5
7.    R->P                    :CONP_2 6
8.    P                       :DIL 2 7
9.  :DD 8

8.9
(P->~P), (R->P), (Q->R), (~Q->R) .: S
1.  SHOW: S
2.   P->~P                    :PR
3.   R->P                     :PR
4.   Q->R                     :PR
5.   ~Q->R                    :PR
6.   Q->P                     :HS 3 4
7.   ~Q->P                    :HS 3 5
8.   P                        :DIL 6 7
9.   ~P                       :MP 2 8
10.  S                        :EFQ 8 9
11. :DD 10

8.10
T .: (((P->Q)->P)->P)
1.  SHOW: ((P->Q)->P)->P
2.   (P->Q)->P                :AS
3.   SHOW: ~~P
4.    ~P                      :AS
5.    ~(P->Q)                 :MT 2 4
6.    P->Q                    :CND_2 4
7.   :ID 5 6
8.   P                        :DNE 3
9.  :CD 8

9.1
(P/\Q) .: (P v Q)
1.  SHOW: P v Q
2.   P/\Q                     :PR
3.   P                        :S 2
4.   P v Q                    :ADD 3
5.  :DD 4

9.2
T .: ~(P/\~P)
1.  SHOW: ~(P/\~P)
2.   P/\~P                    :AS
3.   P                        :S 2
4.   ~P                       :S 2
5.  :ID 3 4

9.3
~Q .: ~(P/\Q)
1.  SHOW: ~(P/\Q)
2.   P/\Q                     :AS
3.   ~Q                       :PR
4.   Q                        :S 2
5.  :ID 3 4

9.4
1.  SHOW: ~(P v Q)
2.   P v Q                    :AS
3.   ~P                       :PR
4.   ~Q                       :PR
5.   ~P/\~Q                   :ADJ 3 4
6.   Q                        :MTP 2 3
7.  :ID 4 6

9.5
~(P v Q) .: ~P
1.  SHOW: ~P
2.   P                        :AS
3.   ~(P v Q)                 :PR
4.   P v Q                    :ADD 2
5.  :ID 3 4

9.6
T .: ((P/\Q)<->(Q/\P))
1.  SHOW: (P/\Q)<->(Q/\P)
2.    SHOW: (P/\Q)->(Q/\P)
3.      P/\Q                  :AS
4.      SHOW: Q/\P
5.        Q                   :S 3
6.        P                   :S 3
7.        Q/\P                :ADJ 5 6
8.      :DD 7
9.    :CD 4
10.   SHOW: (Q/\P)->(P/\Q)
11.     Q/\P                  :AS
12.     SHOW: P/\Q
13.       P                   :S 11
14.       Q                   :S 11
15.       P/\Q                :ADJ 13 14
16.     :DD 15
17.   :CD 12
18.   (P/\Q)<->(Q/\P) :CB 2 10
19. :DD 18

9.7
(P v ~Q), (Q v R), ~P .: R
1.  SHOW: R
2.    P v ~Q                  :PR
3.    Q v R                   :PR
4.    ~P                      :PR
5.    ~Q                      :MTP 2 4
6.    R                       :MTP 3 5
7.  :DD 6

9.8
((P/\Q)->R) .: ((P/\~R)->~Q)
1.  SHOW: (P/\~R)->~Q
2.    P/\~R                   :AS
3.    SHOW: ~Q
4.      Q                     :AS
5.      (P/\Q)->R             :PR
6.      P                     :S 2
7.      P/\Q                  :ADJ 4 6
8.      R                     :MP 5 7
9.      ~R                    :S 2
10.   :ID 8 9
11. :CD 3

9.9
((P/\~R)->~Q) .: ((P/\Q)->R)
1.  SHOW: (P/\Q)->R
2.     P/\Q                   :AS
3.     SHOW: ~~R
4.        ~R                  :AS
5.        (P/\~R)->~Q         :PR
6.        P                   :S 2
7.        P/\~R               :ADJ 4 6
8.        ~Q                  :MP 5 7
9.        Q                   :S 2
10.    :ID 8 9
11.    R                      :DNE 3
12. :CD 11

9.10
(P->Q) .: ((P/\R)->(Q/\R))
1.  SHOW: (P/\R)->(Q/\R)
2.    P/\R                    :AS
3.    SHOW: Q/\R
4.      Q                     :AS
5.      R                     :S 2
6.      Q/\R                  :ADJ 4 5
7.    :CD 6
8.  :CD 3

11.6
~(~P->(Q/\R)), (~S v P) .: ~S
1.  SHOW: ~S
2.    ~(~P->(Q/\R))           :PR
3.    ~S v P                  :PR
4.    ~P/\~(Q/\R)             :NCND_1 2
5.    ~P                      :S 4
6.    ~S                      :MTP 3 5
7.  :DD 6

11.7
((P v Q)->S), ~(R v ~P) .: ~(R<->S)
1.  SHOW: ~(R<->S)
2.    R<->S                   :AS
3.    (P v Q)->S              :PR
4.    ~(R v ~P)               :PR
5.    ~R/\~~P                 :DM_2 4
6.    ~~P                     :S 5
7.    P                       :DNE 6
8.    P v Q                   :ADD 7
9.    ~R                      :S 5
10.   S                       :MP 3 8
11.   S->R                    :BC 2
12.   R                       :MP 10 11
13. :ID 9 12

11.8
((P->Q)->T), (S v T), (P->(S->Q)) .: T
1.  SHOW: T
2.    SHOW: ~~T
3.      ~T                    :AS
4.      (P->Q)->T             :PR
5.      S v T                 :PR
6.      P->(S->Q)             :PR
7.      S                     :MTP 3 5
8.      ~(P->Q)               :MT 3 4
9.      P/\~Q                 :NCND_1 8
10.     P                     :S 9
11.     S->Q                  :MP 6 10
12.     Q                     :MP 7 11
13.     ~Q                    :S 9
14.   :ID 12 13
15.   T                       :DNE 2
16. :DD 15

11.9
((P->Q)->P), (Q->P) .: P
1.  SHOW: P
2.    SHOW: ~~P
3.      ~P                    :AS
4.      (P->Q)->P             :PR
5.      P->Q                  :CND_2 3
6.      ~(P->Q)               :MT 3 4
7.    :ID 5 6
8.    P                       :DNE 2
9.  :DD 8

11.10
~(P->Q), ~(R->Q) .: ~(P->~R)
1.  SHOW: ~(P->~R)
2.    P->~R                   :AS
3.    ~(P->Q)                 :PR
4.    ~(R->Q)                 :PR
5.    P/\~Q                   :NCND_1 3
6.    R/\~Q                   :NCND_1 4
7.    P                       :S 5
8.    R                       :S 6
9.    ~R                      :MP 2 7
10. :ID 8 9

12.1
(P<->S), (~Q->~P), (~R->P) .: (R v (S/\Q))
1.  SHOW: R v (S/\Q)
2.    SHOW: ~~(R v (S/\Q))
3.      ~(R v (S/\Q))         :AS
4.      ~R/\~(S/\Q)           :DM_2 3
5.      ~R                    :S 4
6.      ~(S/\Q)               :S 4
7.      P<->S                 :PR
8.      ~Q->~P                :PR
9.      ~R->P                 :PR
10.     P                     :MP 5 9
11.     ~S v ~Q               :DM_4 6
12.     ~~P                   :DNI 10
13.     ~~Q                   :MT 8 12
14.     ~S                    :MTP 11 13
15.     P->S                  :BC 7
16.     ~P                    :MT 14 15
17.   :ID 10 16
18.   R v (S/\Q)              :DNE 2
19. :DD 18

12.2
(P v S), (S->~(Q->~P)) .: (P v R)
1.  SHOW: P v R
2.    SHOW: ~~P
3.      ~P                    :AS
4.      P v S                 :PR
5.      S                     :MTP 3 4
6.      S->~(Q->~P)           :PR
7.      ~(Q->~P)              :MP 5 6
8.      Q/\~~P                :NCND_1 7
9.      ~~P                   :S 8
10.   :ID 3 9
11.   P                       :DNE 2
12.   P v R                   :ADD 11
13. :DD 12

13.9
T .: (((P->R)/\(Q->S))->((P/\Q)->(R/\S)))
1.  SHOW: ((P->R)/\(Q->S))->((P/\Q)->(R/\S))
2.    (P->R)/\(Q->S)      :AS
3.    SHOW: (P/\Q)->(R/\S)
4.      P/\Q                  :AS
5.      P                     :S 4
6.      Q                     :S 4
7.      P->R                  :S 2
8.      Q->S                  :S 2
9.      R                     :MP 5 7
10.     S                     :MP 6 8
11.     R/\S                  :ADJ 9 10
12.   :CD 11
13. :CD 3

13.10
T .: ((P->(Q<->R))<->((P/\Q)<->(P/\R)))
1.  SHOW: (P->(Q<->R))<->((P/\Q)<->(P/\R))
2.    SHOW: (P->(Q<->R))->((P/\Q)<->(P/\R))
3.      P->(Q<->R)                      :AS
4.      SHOW: (P/\Q)<->(P/\R)
5.        SHOW: (P/\Q)->(P/\R)
6.          P/\Q                        :AS
7.          P                           :S 6
8.          Q                           :S 6
9.          Q<->R                       :MP 3 7
10          Q->R                        :BC 9
11.         R                           :MP 8 10
12.         P/\R                        :ADJ 7 11
13.       :CD 12
14.       SHOW: (P/\R)->(P/\Q)
15.         P/\R                        :AS
16.         P                           :S 15
17.         R                           :S 15
18.         Q<->R                       :MP 3 16
19.         R->Q                        :BC 18
20.         Q                           :MP 17 19
21.         P/\Q                        :ADJ 16 20
22.       :CD 21
23.       (P/\Q)<->(P/\R)               :CB 5 14
24.     :DD 23
25.   :CD 4
26.   SHOW: ((P/\Q)<->(P/\R))->(P->(Q<->R))
27.     (P/\Q)<->(P/\R)                 :AS
28.     (P/\Q)->(P/\R)                  :BC 27
29.     (P/\R)->(P/\Q)                  :BC 27
30.     SHOW: P->(Q<->R)
31.       P                             :AS
32.       SHOW: Q->R
33.         Q                           :AS
34.         P/\Q                        :ADJ 31 33
35.         P/\R                        :MP 28 34
36.         R                           :S 35
37.       :CD 36
38.       SHOW: R->Q
39.         R                           :AS
40.         P/\R                        :ADJ 31 39
41.         P/\Q                        :MP 29 40
42.         Q                           :S 41
43.       :CD 42
44.       (Q<->R)                       :CB 32 38
45.     :CD 44
46.   :CD 30
47.   (P->(Q<->R))<->((P/\Q)<->(P/\R))  :CB 2 26
48. :DD 47

14.9
T .: (((P->Q) v R)<->(P->(Q v R)))
1.  SHOW: ((P->Q) v R)<->(P->(Q v R))
2.    SHOW: ((P->Q) v R)->(P->(Q v R))
3.      (P->Q) v R                      :AS
4.      SHOW: ~~(P->(Q v R))
5.        ~(P->(Q v R))                 :AS
6.        P/\~(Q v R)                   :NCND_1 5
7.        ~(Q v R)                      :S 6
8.        ~Q/\~R                        :DM_2 7
9.        P                             :S 6
10.       ~Q                            :S 8
11.       ~(P->Q)                       :NCND_2 9 10
12.       R                             :MTP 3 11
13.       ~R                            :S 8
14.     :ID 12 13
15.     P->(Q v R)                      :DNE 4
16.   :CD 15
17.   SHOW: (P->(Q v R))->((P->Q) v R)
18.     P->(Q v R)                      :AS
19.     SHOW: ~~((P->Q) v R)
20.       ~((P->Q) v R)                 :AS
21.       ~(P->Q)/\~R                   :DM_2 20
22.       ~(P->Q)                       :S 21
23.       P/\~Q                         :NCND_1 22
24.       P                             :S 23
25.       ~Q                            :S 23
26.       ~R                            :S 21
27.       ~Q/\~R                        :ADJ 25 26
28.       ~(Q v R)                      :DM_1 27
29.       ~(P->(Q v R))                 :NCND_2 24 28
30.     :ID 18 29
31.     (P->Q) v R                      :DNE 19
32.   :CD 31
33.   ((P->Q) v R)<->(P->(Q v R)) :CB 2 17
34. :DD 33

14.10
(P<->Q), (P<->R) .: (P<->(Q v R))
1.  SHOW: P<->(Q v R)
2.    P<->Q                   :PR
3.    P<->R                   :PR
4.    P->Q                    :BC 2
5.    Q->P                    :BC 2
6.    R->P                    :BC 3
7.    SHOW: P->(Q v R)
8.      P                     :AS
9.      Q                     :MP 4 8
10      Q v R                 :ADD 9
11.   :CD 10
12.   SHOW: (Q v R)->P
13.     Q v R                 :AS
14.     P                     :CASES 5 6 13
15.   :CD 14
16.   P<->(Q v R)             :CB 7 12
17. :DD 16

16.1
Ax(F(x)/\G(x)) .: F(c)
1.  SHOW: F(c)
2.    Ax(F(x)/\G(x))          :PR
3.    F(c)/\G(c)              :UI 2
4.    F(c)                    :S 3
5.  :DD 4

16.2
AxF(x), (F(c)->G(c)) .: G(c)
1.  SHOW: G(c)
2.    AxF(x)                  :PR
3.    F(c)->G(c)              :PR
4.    F(c)                    :UI 2
5.    G(c)                    :MP 3 4
6.  :DD 5

16.3
AxF(x), ((F(b)/\F(c))->G(c)) .: ExG(x)
1.  SHOW: ExG(x)
2.    AxF(x)                  :PR
3.    (F(b)/\F(c))->G(c)      :PR
4.    F(b)                    :UI 2
5.    F(c)                    :UI 2
6.    F(b)/\F(c)              :ADJ 4 5
7.    G(c)                    :MP 3 6
8.    ExG(x)                  :EG 7
9.  :DD 8

16.4
AxAy(F(x)->G(y)), F(c) .: G(d)
1.  SHOW: G(d)
2.    AxAy(F(x)->G(y))        :PR
3.    F(c)                    :PR
4.    Ay(F(c)->G(y))          :UI 2
5.    F(c)->G(d)              :UI 4
6.    G(d)                    :MP 3 5
7.  :DD 6

16.5
AxAy(F(x)<->G(y)), F(c) .: F(d)
1.  SHOW: F(d)
2.    AxAy(F(x)<->G(y))       :PR
3.    F(c)                    :PR
4.    Ay(F(c)<->G(y))         :UI 2
5.    Ay(F(d)<->G(y))         :UI 2
6.    F(c)<->G(d)             :UI 4
7.    F(d)<->G(d)             :UI 5
8.    F(c)->G(d)              :BC 6
9.    G(d)->F(d)              :BC 7
10.   F(c)->F(d)              :HS 8 9
11.   F(d)                    :MP 3 10
12. :DD 11

17.1
Ax(F(x)->G(x)), AxF(x) .: AxG(x)
1.  SHOW: AxG(x)
2.    Ax(F(x)->G(x))          :PR
3.    AxF(x)                  :PR
4.    F(c)->G(c)              :UI 2
5.    F(c)                    :UI 3
6.    G(c)                    :MP 4 5
7.  :UD 6

17.2
Ax(F(x)->G(x)), Ax(G(x)->H(x)) .: Ax(F(x)->H(x))
1.  SHOW: Ax(F(x)->H(x))
2.    Ax(F(x)->G(x))          :PR
3.    Ax(G(x)->H(x))          :PR
4.    F(c)->G(c)              :UI 2
5.    G(c)->H(c)              :UI 3
6.    F(c)->H(c)              :HS 4 5
7.  :UD 6

17.3
Ax(G(x)/\G(c)) .: AxG(x)
1.  SHOW: AxG(x)
2.    Ax(G(x)/\G(c))          :PR
3.    G(a)/\G(c)              :UI 2
4.    G(a)                    :S 3
5.  :UD 4

17.4
Ax~F(x), F(d) .: ~AxF(x)
1.  SHOW: ~AxF(x)
2.    Ax~F(x)                 :PR
3.    F(d)                    :PR
4.    ~F(d)                   :UI 2
5.    ~AxF(x)                 :EFQ 3 4
6.  :DD 5

17.5
~ExF(x) .: Ax~F(x)
1.  SHOW: Ax~F(x)
2.    ~ExF(x)                 :PR
3.    Ax~F(x)                 :QN_1 2
4.  :DD 3

17.6
Ex(F(x)/\G(a)) .: G(a)
1.  SHOW: G(a)
2.    Ex(F(x)/\G(a))          :PR
3.    SHOW: G(a)
4.      F(b)/\G(a)            :AS
5.      G(a)                  :S 4
6.    :ED 2 4 5
7.  :DD 3

17.7
Ax(F(x)->G(x)), ExF(x) .: ExG(x)
1.  SHOW: ExG(x)
2.    Ax(F(x)->G(x))          :PR
3.    ExF(x)                  :PR
4.    SHOW: ExG(x)
5.      F(c)                  :AS
6.      F(c)->G(c)            :UI 2
7.      G(c)                  :MP 5 6
8.      ExG(x)                :EG 7
9.    :ED 3 5 8
10. :DD 4

17.8
Ax(F(x)->G(x)), Ex(F(x)/\H(x)) .: Ex(G(x)/\H(x))
1.  SHOW: Ex(G(x)/\H(x))
2.    Ax(F(x)->G(x))          :PR
3.    Ex(F(x)/\H(x))          :PR
4.    SHOW: Ex(G(x)/\H(x))
5.      F(c)/\H(c)            :AS
6.      F(c)->G(c)            :UI 2
7.      F(c)                  :S 5
8.      H(c)                  :S 5
9.      G(c)                  :MP 6 7
10.     G(c)/\H(c)            :ADJ 8 9
11.     Ex(G(x)/\H(x))        :EG 10
12.   :ED 3 5 11
13. :DD 4

17.9
Ax(F(x)->G(x)), ~Ex(F(x)/\G(x)) .: ~ExF(x)
1.  SHOW: ~ExF(x)
2.    Ax(F(x)->G(x))          :PR
3.    ~Ex(F(x)/\G(x))         :PR
4.    SHOW: ~ExF(x)
5.      ExF(x)                :AS
6.      SHOW: Ex(F(x)/\G(x))
7.        F(c)                :AS
8.        F(c)->G(c)          :UI 2
9.        G(c)                :MP 7 8
10        F(c)/\G(c)          :ADJ 7 9
11.       Ex(F(x)/\G(x))      :EG 10
12.     :ED 5 7 11
13.   :ID 3 6
14. :DD 4

17.10
Ex~F(x) .: ~AxF(x)
1.  SHOW: ~AxF(x)
2.    Ex~F(x)                 :PR
3.    SHOW: ~AxF(x)
4.      AxF(x)                :AS
5.      F(x)                  :UI 4
6.      ExF(x)                :EG 5
7.      SHOW: ~ExF(x)
8.        ~F(x)               :AS
9.        ~ExF(x)             :EFQ 5 8
10.     :ED 2 8 9
11.   :ID 6 7
12. :DD 3

0.1
Ax(F(x)->G(x)), Ex(H(x)/\~G(x)) .: Ex(H(x)/\~F(x))
1.  SHOW: Ex(H(x)/\~F(x))
2.    Ax(F(x)->G(x))          :PR
3.    Ex(H(x)/\~G(x))         :PR
4.    SHOW: Ex(H(x)/\~F(x))
5.      H(x)/\~G(x)           :AS
6.      F(x)->G(x)            :UI 2
7.      H(x)                  :S 5
8.      ~G(x)                 :S 5
9.      ~F(x)                 :MT 6 8
10.     H(x)/\~F(x)           :ADJ 7 9
11.     Ex(H(x)/\~F(x))       :EG 10
12.   :ED 3 5 11
13. :DD 4

0.2
Ex(F(x)/\~G(x)), Ax(F(x)->H(x)) .: Ex(H(x)/\~G(x))
1.  SHOW: Ex(H(x)/\~G(x))
2.    Ex(F(x)/\~G(x))         :PR
3.    Ax(F(x)->H(x))          :PR
4.    SHOW: Ex(H(x)/\~G(x))
5.      F(x)/\~G(x)           :AS
6.      F(x)->H(x)            :UI 3
7.      F(x)                  :S 5
8.      H(x)                  :MP 6 7
9.      ~G(x)                 :S 5
10.     H(x)/\~G(x)           :ADJ 8 9
11.     Ex(H(x)/\~G(x))       :EG 10
12.   :ED 2 5 11
13. :DD 4

0.3
Ax(F(x)->G(x)), ~Ex(G(x)/\H(x)) .: ~Ex(H(x)/\F(x))
1.  SHOW: ~Ex(H(x)/\F(x))
2.    Ex(H(x)/\F(x))          :AS
3.    Ax(F(x)->G(x))          :PR
4.    ~Ex(G(x)/\H(x))         :PR
5.    SHOW: Ex(G(x)/\H(x))
6.      H(x)/\F(x)            :AS
7.      F(x)->G(x)            :UI 3
8.      H(x)                  :S 6
9.      F(x)                  :S 6
10.     G(x)                  :MP 7 9
11.     G(x)/\H(x)            :ADJ 8 10
12.     Ex(G(x)/\H(x))        :EG 11
13.   :ED 2 6 12
14. :ID 4 5

0.4
Ax(H(x)->F(x)), ~Ex(F(x)/\G(x)) .: ~Ex(H(x)/\G(x))
1.  SHOW: ~Ex(H(x)/\G(x))
2.    Ex(H(x)/\G(x))          :AS
3.    Ax(H(x)->F(x))          :PR
4.    ~Ex(F(x)/\G(x))         :PR
5.    SHOW: Ex(F(x)/\G(x))
6.      H(x)/\G(x)            :AS
7.      H(x)->F(x)            :UI 3
8.      H(x)                  :S 6
9.      F(x)                  :MP 7 8
10.     G(x)                  :S 6
11.     F(x)/\G(x)            :ADJ 9 10
12.     Ex(F(x)/\G(x))        :EG 11
13.   :ED 2 6 12
14. :ID 4 5

0.5
~Ex(F(x)/\G(x)), Ex(H(x)/\F(x)) .: Ex(H(x)/\~G(x))
1.  SHOW: Ex(H(x)/\~G(x))
2.    ~Ex(F(x)/\G(x))         :PR
3.    Ex(H(x)/\F(x))          :PR
4.    Ax~(F(x)/\G(x))         :QN_1 2
5.    SHOW: Ex(H(x)/\~G(x))
6.      H(x)/\F(x)            :AS
7.      ~(F(x)/\G(x))         :UI 4
8.      ~F(x) v ~G(x)         :DM_4 7
9.      F(x)                  :S 6
10.     ~~F(x)                :DNI 9
11.     H(x)                  :S 6
12.     ~G(x)                 :MTP 8 10
13.     H(x)/\~G(x)           :ADJ 11 12
14.     Ex(H(x)/\~G(x))       :EG 13
15.   :ED 3 6 14
16. :DD 5

0.6
T .: (Ax(F(x)/\G(x)))<->(AxF(x)/\AxG(x))
1.  SHOW: (Ax(F(x)/\G(x)))<->(AxF(x)/\AxG(x))
2.    SHOW: Ax(F(x)/\G(x))->(AxF(x)/\AxG(x))
3.      Ax(F(x)/\G(x))                    :AS
4.      F(x)/\G(x)                        :UI 3
5.      SHOW: AxF(x)
6.        F(x)                            :S 4
7.      :UD 6
8.      SHOW: AxG(x)
9.        G(x)                            :S 4
10.     :UD 9
11.     AxF(x)/\AxG(x)                    :ADJ 5 8
12.   :CD 11
13.   SHOW: (AxF(x)/\AxG(x))->Ax(F(x)/\G(x))
14.     AxF(x)/\AxG(x)                    :AS
15.     AxF(x)                            :S 14
16.     AxG(x)                            :S 14
17.     F(x)                              :UI 15
18.     G(x)                              :UI 16
19.     SHOW: Ax(F(x)/\G(x))
20.       F(x)/\G(x)                      :ADJ 17 18
21.     :UD 20
22.   :CD 19
23.   (Ax(F(x)/\G(x)))<->(AxF(x)/\AxG(x)) :CB 2 13
24. :DD 23

0.11
ExF(x)->ExG(x) .: Ex(F(x)-> G(x))
1.  SHOW: Ex(F(x)->G(x))
2.    SHOW: ~~Ex(F(x)->G(x))
3.      ~Ex(F(x)->G(x))       :AS
4.      ExF(x)->ExG(x)        :PR
5.      Ax~(F(x)->G(x))       :QNONE 3
6.      ~(F(c)->G(c))         :UI 5
7.      F(c)/\~G(c)           :NEGCONONE 6
8.      F(c)                  :S 7
9.      ExF(x)                :EG 8
10.     ExG(x)                :MP 4 9
11.     SHOW: Ex(F(x)->G(x))
12.       G(c)                :AS
13.       F(c)->G(c)          :CONONE 12
14.       Ex(F(x)->G(x))      :EG 13
15.     :ED 10 12 14
16.   :ID 3 11
17.   Ex(F(x)->G(x))          :DNE 2
18. :DD 17