Theorem
axc16gb
Biconditional strengthening of
axc16g
. (Contributed by NM, 15-May-1993.)
Conclusion
\( \vdash \forall x \, x = y' \rightarrow (\varphi \leftrightarrow \forall z \, \varphi) \)
Proof
l0
axc16g
sp
impbid1
l0
_
This is the content in the right pane.