Axiom ax-frege52a 38151

Description: The case when the content of ph is identical with the content of ps and in which a proposition controlled by an element for which we substitute the content of ph is affirmed ( in this specific case the identity logical funtion ) and the same proposition, this time where we substituted the content of ps, is denied does not take place. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-frege52a	|- ( ( ph <-> ps ) -> (if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )

Detailed syntax breakdown of Axiom ax-frege52a

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3	1, 2	wb 196	. 2 wff ( ph <-> ps )
4		wth	. . . 4 wff th
5		wch	. . . 4 wff ch
6	1, 4, 5	wif 1012	. . 3 wff if- ( ph , th , ch )
7	2, 4, 5	wif 1012	. . 3 wff if- ( ps , th , ch )
8	6, 7	wi 4	. 2 wff (if- ( ph , th , ch ) -> if- ( ps , th , ch ) )
9	3, 8	wi 4	1 wff ( ( ph <-> ps ) -> (if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )

This axiom is referenced by:  frege52aid  38152  frege53a  38154  frege57a  38167