Theorem ax12ev2c

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

Conclusion
\( \vdash x' = y \rightarrow \exists y \, (x' = y \wedge \varphi) \rightarrow \varphi \)
Proof
l0
equcomi
\( \vdash x' = y \rightarrow y = x' \)
anim1i _
l2
eximi _
\( \vdash \exists y \, (x' = y \wedge \varphi) \rightarrow \exists y \, (y = x' \wedge \varphi) \)
ax12ev2
\( \vdash \exists y \, (y = x' \wedge \varphi) \rightarrow y = x' \rightarrow \varphi \)
syl2imc l2 l0 _