Metamath Proof Explorer


Theorem bj-exalims

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 ) ) )

Proof

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 ) ) )