1:: | |- (. A e. B ->. A e. B ).
|
2:: | |- (. A e. B ,. C e. D ->. C e. D ).
|
3:: | |- (. A e. B ,. C e. D ,. A. x e. B
A. y e. D ph ->. A. x e. B A. y e. D ph ).
|
4:1,3,?: e13 | |- (. A e. B ,. C e. D ,. A. x e. B
A. y e. D ph ->. [. A / x ]. A. y e. D ph ).
|
5:1,4,?: e13 | |- (. A e. B ,. C e. D ,. A. x e. B
A. y e. D ph ->. A. y e. D [. A / x ]. ph ).
|
6:2,5,?: e23 | |- (. A e. B ,. C e. D ,. A. x e. B
A. y e. D ph ->. [. C / y ]. [. A / x ]. ph ).
|
7:6: | |- (. A e. B ,. C e. D ->. ( A. x e. B
A. y e. D ph -> [. C / y ]. [. A / x ]. ph ) ).
|
8:7: | |- (. A e. B ->. ( C e. D
-> ( A. x e. B A. y e. D ph -> [. C / y ]. [. A / x ]. ph ) ) ).
|
qed:8: | |- ( A e. B -> ( C e. D
-> ( A. x e. B A. y e. D ph -> [. C / y ]. [. A / x ]. ph ) ) )
|