Metamath Proof Explorer


Theorem bj-nnflemee

Description: One of four lemmas for nonfreeness: antecedent and consequent both expressed using existential quantifier. (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-nnflemee x y φ φ y x φ x φ

Proof

Step Hyp Ref Expression
1 excom y x φ x y φ
2 exim x y φ φ x y φ x φ
3 1 2 syl5bi x y φ φ y x φ x φ