Metamath Proof Explorer

Theorem frege66b

Description: Swap antecedents of frege65b . Proposition 66 of Frege1879 p. 54. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	frege66b	\|- ( A. x ( ph -> ps ) -> ( A. x ( ch -> ph ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege65b	\|- ( A. x ( ch -> ph ) -> ( A. x ( ph -> ps ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) )
2		ax-frege8	\|- ( ( A. x ( ch -> ph ) -> ( A. x ( ph -> ps ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) ) -> ( A. x ( ph -> ps ) -> ( A. x ( ch -> ph ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) ) )
3	1 2	ax-mp	\|- ( A. x ( ph -> ps ) -> ( A. x ( ch -> ph ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) )

Step

Hyp

Ref

Expression

frege65b

 |-  ( A. x ( ch -> ph ) -> ( A. x ( ph -> ps ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) )

ax-frege8

 |-  ( ( A. x ( ch -> ph ) -> ( A. x ( ph -> ps ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) ) -> ( A. x ( ph -> ps ) -> ( A. x ( ch -> ph ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) ) )

1 2

ax-mp

 |-  ( A. x ( ph -> ps ) -> ( A. x ( ch -> ph ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) )