Metamath Proof Explorer


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 x φ φ

Proof

Step Hyp Ref Expression
1 ax-frege58b x φ x x φ
2 sbid x x φ φ
3 2 biimpi x x φ φ
4 1 3 syl x φ φ