Metamath Proof Explorer

Theorem frege53a

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

		Ref	Expression
	Assertion	frege53a	\|- ( if- ( ph , th , ch ) -> ( ( ph <-> ps ) -> if- ( ps , th , ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-frege52a	\|- ( ( ph <-> ps ) -> ( if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )
2		ax-frege8	\|- ( ( ( ph <-> ps ) -> ( if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) ) -> ( if- ( ph , th , ch ) -> ( ( ph <-> ps ) -> if- ( ps , th , ch ) ) ) )
3	1 2	ax-mp	\|- ( if- ( ph , th , ch ) -> ( ( ph <-> ps ) -> if- ( ps , th , ch ) ) )

Step

Hyp

Ref

Expression

ax-frege52a

 |-  ( ( ph <-> ps ) -> ( if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )

ax-frege8

 |-  ( ( ( ph <-> ps ) -> ( if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) ) -> ( if- ( ph , th , ch ) -> ( ( ph <-> ps ) -> if- ( ps , th , ch ) ) ) )

1 2

ax-mp

 |-  ( if- ( ph , th , ch ) -> ( ( ph <-> ps ) -> if- ( ps , th , ch ) ) )