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	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ax-frege58b	⊢ ( ∀ 𝑥 𝜑 → [ 𝑥 / 𝑥 ] 𝜑 )
2		sbid	⊢ ( [ 𝑥 / 𝑥 ] 𝜑 ↔ 𝜑 )
3	2	biimpi	⊢ ( [ 𝑥 / 𝑥 ] 𝜑 → 𝜑 )
4	1 3	syl	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )