1:: | |- (. A e. B ->. A e. B ).
|
2:1,?: e1a | |- (. A e. B ->. ( [. A / x ]. ( ( ph
\/ ps ) \/ ch ) <-> ( [. A / x ]. ( ph \/ ps )
\/ [. A / x ]. ch ) ) ).
|
3:: | |- ( ( ( ph \/ ps ) \/ ch ) <-> ( ph
\/ ps \/ ch ) )
|
32:3: | |- A. x ( ( ( ph \/ ps ) \/ ch )
<-> ( ph \/ ps \/ ch ) )
|
33:1,32,?: e10 | |- (. A e. B ->. [. A / x ]. ( ( ( ph
\/ ps ) \/ ch ) <-> ( ph \/ ps \/ ch ) ) ).
|
4:1,33,?: e11 | |- (. A e. B ->. ( [. A / x ]. ( ( ph
\/ ps ) \/ ch ) <-> [. A / x ]. ( ph \/ ps \/ ch ) ) ).
|
5:2,4,?: e11 | |- (. A e. B ->. ( [. A / x ]. ( ph
\/ ps \/ ch ) <-> ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) ) ).
|
6:1,?: e1a | |- (. A e. B ->. ( [. A / x ]. ( ph
\/ ps ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps ) ) ).
|
7:6,?: e1a | |- (. A e. B ->. ( ( [. A / x ]. ( ph
\/ ps ) \/ [. A / x ]. ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps )
\/ [. A / x ]. ch ) ) ).
|
8:5,7,?: e11 | |- (. A e. B ->. ( [. A / x ]. ( ph
\/ ps \/ ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps )
\/ [. A / x ]. ch ) ) ).
|
9:?: | |- ( ( ( [. A / x ]. ph
\/ [. A / x ]. ps ) \/ [. A / x ]. ch ) <-> ( [. A / x ]. ph
\/ [. A / x ]. ps \/ [. A / x ]. ch ) )
|
10:8,9,?: e10 | |- (. A e. B ->. ( [. A / x ]. ( ph
\/ ps \/ ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps
\/ [. A / x ]. ch ) ) ).
|
qed:10: | |- ( A e. B -> ( [. A / x ]. ( ph
\/ ps \/ ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps
\/ [. A / x ]. ch ) ) )
|