Metamath Proof Explorer

Theorem frege60b

Description: Swap antecedents of ax-frege58b . Proposition 60 of Frege1879 p. 52. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	frege60b	$⊢ \forall x (φ \to (ψ \to χ)) \to ([y/ x] ψ \to ([y/ x] φ \to [y/ x] χ))$

Proof

Step	Hyp	Ref	Expression
1		ax-frege58b	$⊢ \forall x (φ \to (ψ \to χ)) \to [y/ x] (φ \to (ψ \to χ))$
2		sbim	$⊢ [y/ x] (φ \to (ψ \to χ)) \leftrightarrow ([y/ x] φ \to [y/ x] (ψ \to χ))$
3		sbim	$⊢ [y/ x] (ψ \to χ) \leftrightarrow ([y/ x] ψ \to [y/ x] χ)$
4	3	imbi2i	$⊢ ([y/ x] φ \to [y/ x] (ψ \to χ)) \leftrightarrow ([y/ x] φ \to ([y/ x] ψ \to [y/ x] χ))$
5	2 4	bitri	$⊢ [y/ x] (φ \to (ψ \to χ)) \leftrightarrow ([y/ x] φ \to ([y/ x] ψ \to [y/ x] χ))$
6	1 5	sylib	$⊢ \forall x (φ \to (ψ \to χ)) \to ([y/ x] φ \to ([y/ x] ψ \to [y/ x] χ))$
7		frege12	$⊢ (\forall x (φ \to (ψ \to χ)) \to ([y/ x] φ \to ([y/ x] ψ \to [y/ x] χ))) \to (\forall x (φ \to (ψ \to χ)) \to ([y/ x] ψ \to ([y/ x] φ \to [y/ x] χ)))$
8	6 7	ax-mp	$⊢ \forall x (φ \to (ψ \to χ)) \to ([y/ x] ψ \to ([y/ x] φ \to [y/ x] χ))$