Theorem
sbequ12
An equality theorem for substitution. (Contributed by NM, 14-May-1993.)
Conclusion
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow [ y' / x ] \, \varphi) \)
Proof
l0
sbequ1
sbequ2
impbid
l0
_
This is the content in the right pane.