Theorem frege58bid

Description: If A. x ph is affirmed, ph cannot be denied. Identical to sp . See ax-frege58b and frege58c for versions which more closely track the original. Axiom 58 of Frege1879 p. 51. (Contributed by RP, 28-Mar-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	frege58bid	$$⊢\forall x\phi \to \phi$$

Proof

Step	Hyp	Ref	Expression
1		ax-frege58b	$$⊢\forall x\phi \to \left[x/x\right]\phi$$
2		sbid	$$⊢\left[x/x\right]\phi \leftrightarrow \phi$$
3	2	biimpi	$$⊢\left[x/x\right]\phi \to \phi$$
4	1 3	syl	$$⊢\forall x\phi \to \phi$$