Theorem frege57c

Description: Swap order of implication in ax-frege52c . Proposition 57 of Frege1879 p. 51. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		frege57c.a	|- A e. C
2		ax-frege52c	|- ( B = A -> ( [. B / x ]. ph -> [. A / x ]. ph ) )
3	1	frege56c	|- ( ( B = A -> ( [. B / x ]. ph -> [. A / x ]. ph ) ) -> ( A = B -> ( [. B / x ]. ph -> [. A / x ]. ph ) ) )
4	2 3	ax-mp	|- ( A = B -> ( [. B / x ]. ph -> [. A / x ]. ph ) )