1:: | |- (. ( ph <-> ps ) ->. ( ph <-> ps ) ).
|
2:: | |- (. ( ph <-> ps ) ,. ( ch <-> th )
->. ( ch <-> th ) ).
|
3:: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ph
-> ch ) ->. ( ph -> ch ) ).
|
4:1,3: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ph
-> ch ) ->. ( ps -> ch ) ).
|
5:2,4: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ph
-> ch ) ->. ( ps -> th ) ).
|
6:5: | |- (. ( ph <-> ps ) ,. ( ch <-> th )
->. ( ( ph -> ch ) -> ( ps -> th ) ) ).
|
7:: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ps
-> th ) ->. ( ps -> th ) ).
|
8:1,7: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ps
-> th ) ->. ( ph -> th ) ).
|
9:2,8: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ps
-> th ) ->. ( ph -> ch ) ).
|
10:9: | |- (. ( ph <-> ps ) ,. ( ch <-> th )
->. ( ( ps -> th ) -> ( ph -> ch ) ) ).
|
11:6,10: | |- (. ( ph <-> ps ) ,. ( ch <-> th )
->. ( ( ph -> ch ) <-> ( ps -> th ) ) ).
|
12:11: | |- (. ( ph <-> ps ) ->. ( ( ch <-> th )
-> ( ( ph -> ch ) <-> ( ps -> th ) ) ) ).
|
qed:12: | |- ( ( ph <-> ps ) -> ( ( ch <-> th )
-> ( ( ph -> ch ) <-> ( ps -> th ) ) ) )
|