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 
|- ( ( ps /\ ch ) -> if- ( ph , ps , ch ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wps 
 |-  ps
1 wch 
 |-  ch
2 0 1 wa 
 |-  ( ps /\ ch )
3 wph 
 |-  ph
4 3 0 1 wif 
 |-  if- ( ph , ps , ch )
5 2 4 wi 
 |-  ( ( ps /\ ch ) -> if- ( ph , ps , ch ) )