Metamath Proof Explorer

Theorem sptruw

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

Ref Expression
Hypothesis sptruw.1 
|- ph
Assertion sptruw 
|- ( A. x ph -> ph )

Proof

Step Hyp Ref Expression
1 sptruw.1 
 |-  ph
2 1 a1i 
 |-  ( A. x ph -> ph )