Metamath Proof Explorer

Theorem frege53c

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

		Ref	Expression
	Assertion	frege53c	\|- ( [. A / x ]. ph -> ( A = B -> [. B / x ]. ph ) )

Step	Hyp	Ref	Expression
1		ax-frege52c	\|- ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) )
2		ax-frege8	\|- ( ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) -> ( [. A / x ]. ph -> ( A = B -> [. B / x ]. ph ) ) )
3	1 2	ax-mp	\|- ( [. A / x ]. ph -> ( A = B -> [. B / x ]. ph ) )

Step

Hyp

Ref

Expression

 |-  ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) )

 |-  ( ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) -> ( [. A / x ]. ph -> ( A = B -> [. B / x ]. ph ) ) )

1 2

 |-  ( [. A / x ]. ph -> ( A = B -> [. B / x ]. ph ) )