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