Theorem sptruw

Version of sp when \( \varphi \) is true. Instance of a1i. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.)

Hypothesis

sptruw.1

\( \vdash \varphi \)

Conclusion

\( \vdash \forall x \, \varphi \rightarrow \varphi \)

Proof

sptruw.1

a1i _