Description: Distributing quantifiers over a nested implication. (Almost) the general statement that spimfw proves. (Contributed by BJ, 29-Sep-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bj-exalims.1 | |- ( E. x ph -> ( -. ch -> A. x -. ch ) ) |
|
Assertion | bj-exalims | |- ( A. x ( ph -> ( ps -> ch ) ) -> ( E. x ph -> ( A. x ps -> ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-exalims.1 | |- ( E. x ph -> ( -. ch -> A. x -. ch ) ) |
|
2 | bj-exalim | |- ( A. x ( ph -> ( ps -> ch ) ) -> ( E. x ph -> ( A. x ps -> E. x ch ) ) ) |
|
3 | eximal | |- ( ( E. x ch -> ch ) <-> ( -. ch -> A. x -. ch ) ) |
|
4 | 1 3 | sylibr | |- ( E. x ph -> ( E. x ch -> ch ) ) |
5 | 4 | a1i | |- ( A. x ( ph -> ( ps -> ch ) ) -> ( E. x ph -> ( E. x ch -> ch ) ) ) |
6 | 2 5 | syldd | |- ( A. x ( ph -> ( ps -> ch ) ) -> ( E. x ph -> ( A. x ps -> ch ) ) ) |