1:: | |- (. ( ph -> A. x ph )
->. ( ph -> A. x ph ) ).
|
2:: | |- (. ( ph -> A. x ph ) ,. ( ps /\ ph
/\
ch ) ->. ( ps /\ ph /\ ch ) ).
|
3:2,?: e2 | |- (. ( ph -> A. x ph ) ,. ( ps
/\ ph /\ ch ) ->. ps ).
|
4:2,?: e2 | |- (. ( ph -> A. x ph ) ,. ( ps
/\ ph /\ ch ) ->. ph ).
|
5:2,?: e2 | |- (. ( ph -> A. x ph ) ,. ( ps
/\ ph /\ ch ) ->. ch ).
|
6:1,4,?: e12 | |- (. ( ph -> A. x ph ) ,. ( ps
/\ ph /\ ch ) ->. A. x ph ).
|
7:3,?: e2 | |- (. ( ph -> A. x ph ) ,. ( ps
/\ ph /\ ch ) ->. A. x ps ).
|
8:5,?: e2 | |- (. ( ph -> A. x ph ) ,. ( ps
/\ ph /\ ch ) ->. A. x ch ).
|
9:7,6,8,?: e222 | |- (. ( ph -> A. x ph ) ,. ( ps
/\ ph /\ ch ) ->. ( A. x ps /\ A. x ph /\ A. x ch ) ).
|
10:9,?: e2 | |- (. ( ph -> A. x ph ) ,. ( ps
/\ ph /\ ch ) ->. A. x ( ps /\ ph /\ ch ) ).
|
11:10:in2 | |- (. ( ph -> A. x ph ) ->. ( ( ps
/\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) ).
|
qed:11:in1 | |- ( ( ph -> A. x ph ) -> ( ( ps
/\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )
|