Axiom ax-frege52a 37171

Description: The case when the content of 𝜑 is identical with the content of 𝜓 and in which a proposition controlled by an element for which we substitute the content of 𝜑 is affirmed ( in this specific case the identity logical funtion ) and the same proposition, this time where we subsituted the content of 𝜓, 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	⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒)))

Detailed syntax breakdown of Axiom ax-frege52a

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wb 195	. 2 wff (𝜑 ↔ 𝜓)
4		wth	. . . 4 wff 𝜃
5		wch	. . . 4 wff 𝜒
6	1, 4, 5	wif 1006	. . 3 wff if-(𝜑, 𝜃, 𝜒)
7	2, 4, 5	wif 1006	. . 3 wff if-(𝜓, 𝜃, 𝜒)
8	6, 7	wi 4	. 2 wff (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒))
9	3, 8	wi 4	1 wff ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒)))

This axiom is referenced by:  frege52aid  37172  frege53a  37174  frege57a  37187