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	⊢ 𝜓
1		wch	⊢ 𝜒
2	0 1	wa	⊢ ( 𝜓 ∧ 𝜒 )
3		wph	⊢ 𝜑
4	3 0 1	wif	⊢ if- ( 𝜑 , 𝜓 , 𝜒 )
5	2 4	wi	⊢ ( ( 𝜓 ∧ 𝜒 ) → if- ( 𝜑 , 𝜓 , 𝜒 ) )