Metamath Proof Explorer

Theorem bj-alcomexcom

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 x y ¬ φ y x ¬ φ y x φ x y φ


Step Hyp Ref Expression
1 2nexaln ¬ x y φ x y ¬ φ
2 2nexaln ¬ y x φ y x ¬ φ
3 1 2 imbi12i ¬ x y φ ¬ y x φ x y ¬ φ y x ¬ φ
4 con4 ¬ x y φ ¬ y x φ y x φ x y φ
5 3 4 sylbir x y ¬ φ y x ¬ φ y x φ x y φ