Theorem ax12b

A bidirectional version of axc15. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)

Conclusion
\( \vdash \neg \forall x \, x = y' \wedge x = y' \rightarrow (\varphi \leftrightarrow \forall x \, (x = y' \rightarrow \varphi)) \)
Proof
axc15
l1
imp _
sp
com12 _
adantl _
impbid l1 _