Theorem ax12ev2c

Description: A commuted form of ax12ev2 . (Contributed by BTernaryTau, 8-Sep-2026)

	Ref	Expression
Assertion	ax12ev2c	|- ( x = y -> ( E. y ( x = y /\ ph ) -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		equcomi	|- ( x = y -> y = x )
2	1	anim1i	|- ( ( x = y /\ ph ) -> ( y = x /\ ph ) )
3	2	eximi	|- ( E. y ( x = y /\ ph ) -> E. y ( y = x /\ ph ) )
4		ax12ev2	|- ( E. y ( y = x /\ ph ) -> ( y = x -> ph ) )
5	3 1 4	syl2imc	|- ( x = y -> ( E. y ( x = y /\ ph ) -> ph ) )