Step |
Hyp |
Ref |
Expression |
1 |
|
sbcimg |
|- ( A e. V -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) ) |
2 |
1
|
biimpd |
|- ( A e. V -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) ) |
3 |
|
sbcimg |
|- ( A e. V -> ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) |
4 |
|
imbi2 |
|- ( ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) ) |
5 |
4
|
biimpcd |
|- ( ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) -> ( ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) ) |
6 |
2 3 5
|
syl6ci |
|- ( A e. V -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) ) |
7 |
|
idd |
|- ( A e. V -> ( ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) ) |
8 |
|
biimpr |
|- ( ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( ( [. A / x ]. ps -> [. A / x ]. ch ) -> [. A / x ]. ( ps -> ch ) ) ) |
9 |
3 7 8
|
ee13 |
|- ( A e. V -> ( ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) ) |
10 |
9 1
|
sylibrd |
|- ( A e. V -> ( ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> [. A / x ]. ( ph -> ( ps -> ch ) ) ) ) |
11 |
6 10
|
impbid |
|- ( A e. V -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) ) |