Metamath Proof Explorer


Axiom ax-frege58a

Description: If A. x ph is affirmed, [ y / x ] ph cannot be denied. Identical to stdpc4 . Axiom 58 of Frege1879 p. 51. (Contributed by RP, 28-Mar-2020) (New usage is discouraged.)

Ref Expression
Assertion ax-frege58a ψ χ if- φ ψ χ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wps wff ψ
1 wch wff χ
2 0 1 wa wff ψ χ
3 wph wff φ
4 3 0 1 wif wff if- φ ψ χ
5 2 4 wi wff ψ χ if- φ ψ χ