Description: Distribute quantifiers over a nested implication.
This and the following theorems are the general instances of already proved theorems. They could be moved to the main part, before ax-5 . I propose to move to the main part: bj-exalim , bj-exalimi , bj-exalims , bj-exalimsi , bj-ax12i , bj-ax12wlem , bj-ax12w . A new label is needed for bj-ax12i and label suggestions are welcome for the others. I also propose to change -. A. x -. to E. x in speimfw and spimfw (other spim* theorems use E. x and very few theorems in set.mm use -. A. x -. ). (Contributed by BJ, 8-Nov-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-exalim | |- ( A. x ( ph -> ( ps -> ch ) ) -> ( E. x ph -> ( A. x ps -> E. x ch ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.04 | |- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) ) |
|
| 2 | 1 | alimi | |- ( A. x ( ph -> ( ps -> ch ) ) -> A. x ( ps -> ( ph -> ch ) ) ) |
| 3 | bj-alexim | |- ( A. x ( ps -> ( ph -> ch ) ) -> ( A. x ps -> ( E. x ph -> E. x ch ) ) ) |
|
| 4 | pm2.04 | |- ( ( A. x ps -> ( E. x ph -> E. x ch ) ) -> ( E. x ph -> ( A. x ps -> E. x ch ) ) ) |
|
| 5 | 2 3 4 | 3syl | |- ( A. x ( ph -> ( ps -> ch ) ) -> ( E. x ph -> ( A. x ps -> E. x ch ) ) ) |