Theorem frege56c

Description: Lemma for frege57c . Proposition 56 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	frege56c.b	|- B e. C
Assertion	frege56c	|- ( ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) -> ( B = A -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege56c.b	|- B e. C
2	1	frege54cor1c	|- [. B / x ]. x = B
3		frege53c	|- ( [. B / x ]. x = B -> ( B = A -> [. A / x ]. x = B ) )
4	2 3	ax-mp	|- ( B = A -> [. A / x ]. x = B )
5		frege55lem1c	|- ( ( B = A -> [. A / x ]. x = B ) -> ( B = A -> A = B ) )
6	4 5	ax-mp	|- ( B = A -> A = B )
7		frege9	|- ( ( B = A -> A = B ) -> ( ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) -> ( B = A -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) ) )
8	6 7	ax-mp	|- ( ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) -> ( B = A -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) )