1:: | |- (. ( ph <-> ps ) ->. ( ph <-> ps ) ).
|
2:: | |- (. ( ph <-> ps ) ,. ( ch <-> th )
->. ( ch <-> th ) ).
|
3:: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ta
<-> et ) ->. ( ta <-> et ) ).
|
4:2,3: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ta
<-> et ) ->. ( ( ch -> ta ) <-> ( th -> et ) ) ).
|
5:1,4: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ta
<-> et ) ->. ( ( ph -> ( ch -> ta ) ) <-> ( ps -> ( th -> et ) ) ) ).
|
6:5: | |- (. ( ph <-> ps ) ,. ( ch <-> th )
->. ( ( ta <-> et ) -> ( ( ph -> ( ch -> ta ) ) <-> ( ps -> ( th
-> et ) ) ) ) ).
|
7:6: | |- (. ( ph <-> ps ) ->. ( ( ch <-> th )
-> ( ( ta <-> et ) -> ( ( ph -> ( ch -> ta ) ) <-> ( ps -> ( th
-> et ) ) ) ) ) ).
|
qed:7: | |- ( ( ph <-> ps ) -> ( ( ch <-> th )
-> ( ( ta <-> et ) -> ( ( ph -> ( ch -> ta ) ) <-> ( ps -> ( th
-> et ) ) ) ) ) )
|