1:: | |- (. ( ( ph /\ ps /\ ch )
-> ( th <-> ta ) ) ->. ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) ).
|
2:: | |- ( ( th <-> ta ) <-> ( ta
<-> th ) )
|
3:1,2,?: e10 | |- (. ( ( ph /\ ps /\ ch )
-> ( th <-> ta ) ) ->. ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) ).
|
4:3,?: e1a | |- (. ( ( ph /\ ps /\ ch )
-> ( th <-> ta ) ) ->. ( ph -> ( ps -> ( ch -> ( ta
<-> th ) ) ) ) ).
|
5:4: | |- ( ( ( ph /\ ps /\ ch )
-> ( th <-> ta ) ) -> ( ph -> ( ps -> ( ch -> ( ta
<-> th ) ) ) ) )
|
6:: | |- (. ( ph -> ( ps -> ( ch
-> ( ta <-> th ) ) ) ) ->. ( ph -> ( ps -> ( ch -> ( ta
<-> th ) ) ) ) ).
|
7:6,?: e1a | |- (. ( ph -> ( ps -> ( ch
-> ( ta <-> th ) ) ) ) ->. ( ( ph /\ ps /\ ch ) -> ( ta
<-> th ) ) ).
|
8:7,2,?: e10 | |- (. ( ph -> ( ps -> ( ch
-> ( ta <-> th ) ) ) ) ->. ( ( ph /\ ps /\ ch ) -> ( th
<-> ta ) ) ).
|
9:8: | |- ( ( ph -> ( ps -> ( ch
-> ( ta <-> th ) ) ) ) -> ( ( ph /\ ps /\ ch ) -> ( th
<-> ta ) ) )
|
qed:5,9,?: e00 | |- ( ( ( ph /\ ps /\ ch )
-> ( th <-> ta ) ) <-> ( ph -> ( ps -> ( ch -> ( ta
<-> th ) ) ) ) )
|