Metamath Proof Explorer

Theorem frege53aid

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

		Ref	Expression
	Assertion	frege53aid	$⊢ φ \to ((φ \leftrightarrow ψ) \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		frege52aid	$⊢ (φ \leftrightarrow ψ) \to (φ \to ψ)$
2		ax-frege8	$⊢ ((φ \leftrightarrow ψ) \to (φ \to ψ)) \to (φ \to ((φ \leftrightarrow ψ) \to ψ))$
3	1 2	ax-mp	$⊢ φ \to ((φ \leftrightarrow ψ) \to ψ)$