Metamath Proof Explorer

Theorem alequexv

Description: Version of equs4v with its consequence simplified by exsimpr . (Contributed by BJ, 9-Nov-2021)

Ref Expression
Assertion alequexv x x = y φ x φ


Step Hyp Ref Expression
1 ax6ev x x = y
2 exim x x = y φ x x = y x φ
3 1 2 mpi x x = y φ x φ