1:: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. ( A. x ( ph -> A. x ph ) /\ A. x ( ps ->
A. x ps ) ) ).
|
2:1: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. A. x ( ph -> A. x ph ) ).
|
3:: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) , -. ph ->. -. ph ).
|
4:2: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. A. x ( -. ph -> A. x -. ph ) ).
|
5:4: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. ( -. ph -> A. x -. ph ) ).
|
6:3,5: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) , -. ph ->. A. x -. ph ).
|
7:: | |- ( -. ph -> ( ph -> ps ) )
|
8:7: | |- ( A. x -. ph -> A. x ( ph -> ps ) )
|
9:6,8: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) , -. ph ->. A. x ( ph -> ps ) ).
|
10:9: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. ( -. ph -> A. x ( ph -> ps ) ) ).
|
11:: | |- ( ps -> ( ph -> ps ) )
|
12:11: | |- ( A. x ps -> A. x ( ph -> ps ) )
|
13:1: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. A. x ( ps -> A. x ps ) ).
|
14:13: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. ( ps -> A. x ps ) ).
|
15:14,12: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. ( ps -> A. x ( ph -> ps ) ) ).
|
16:10,15: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. ( ( -. ph \/ ps ) -> A. x ( ph -> ps ) ) ).
|
17:: | |- ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
|
18:16,17: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
|
19:: | |- ( A. x ( ph -> A. x ph ) -> A. x A. x (
ph -> A. x ph ) )
|
20:: | |- ( A. x ( ps -> A. x ps ) -> A. x A. x (
ps -> A. x ps ) )
|
21:19,20: | |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) -> A. x ( A. x ( ph -> A. x ph ) /\ A. x ( ps ->
A. x ps ) ) )
|
22:21,18: | |- (. ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) ->. A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ).
|
qed:22: | |- ( ( A. x ( ph -> A. x ph ) /\ A. x ( ps
-> A. x ps ) ) -> A. x ( ( ph -> ps ) -> A. x ( ph -> ps ) ) )
|