Metamath Proof Explorer

Theorem frege57a

Description: Analogue of frege57aid . Proposition 57 of Frege1879 p. 51. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

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

Step

Hyp

Ref

Expression

ax-frege52a

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

frege56a

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

1 2

ax-mp

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