Theorem sbtALT

Alternate proof of sbt, shorter but using additional axioms. (Contributed by NM, 21-Jan-2004.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
sbtALT.1
\( \vdash \varphi \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \)
Proof
l0
stdpc4
\( \vdash \forall x \, \varphi \rightarrow [ y' / x ] \, \varphi \)
sbtALT.1
\( \vdash \varphi \)
mpg l0 _