Description: Commutation of universal quantifiers implies commutation of existential quantifiers. Can be placed in the ax-4 section, soon after 2nexaln , and used to prove excom . (Contributed by BJ, 29-Nov-2020) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-alcomexcom | |- ( ( A. x A. y -. ph -> A. y A. x -. ph ) -> ( E. y E. x ph -> E. x E. y ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2nexaln | |- ( -. E. x E. y ph <-> A. x A. y -. ph ) |
|
| 2 | 2nexaln | |- ( -. E. y E. x ph <-> A. y A. x -. ph ) |
|
| 3 | 1 2 | imbi12i | |- ( ( -. E. x E. y ph -> -. E. y E. x ph ) <-> ( A. x A. y -. ph -> A. y A. x -. ph ) ) |
| 4 | con4 | |- ( ( -. E. x E. y ph -> -. E. y E. x ph ) -> ( E. y E. x ph -> E. x E. y ph ) ) |
|
| 5 | 3 4 | sylbir | |- ( ( A. x A. y -. ph -> A. y A. x -. ph ) -> ( E. y E. x ph -> E. x E. y ph ) ) |