Theorem sbtlem

In the case of sbt, the hypothesis in [df-sb] is derivable from propositional axioms and [ax-gen] alone. The essential proof step is presented in this lemma. (Contributed by Wolf Lammen, 4-Feb-2026.)

Hypothesis
sbtlem.1
\( \vdash \varphi \)
Conclusion
\( \vdash \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
Proof
sbtlem.1
a1i _
ax-gen _
a1i _
ax-gen _