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
|- ( A. x ph -> ph )

Proof

Step Hyp Ref Expression
1 ax-frege58b
 |-  ( A. x ph -> [ x / x ] ph )
2 sbid
 |-  ( [ x / x ] ph <-> ph )
3 2 biimpi
 |-  ( [ x / x ] ph -> ph )
4 1 3 syl
 |-  ( A. x ph -> ph )