This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm5.4

Description: Antecedent absorption implication. Theorem *5.4 of WhiteheadRussell p. 125. (Contributed by NM, 5-Aug-1993)

		Ref	Expression
	Assertion	pm5.4	$⊢ (φ \to (φ \to ψ)) \leftrightarrow (φ \to ψ)$

Step	Hyp	Ref	Expression
1		pm5.5	$⊢ φ \to ((φ \to ψ) \leftrightarrow ψ)$
2	1	pm5.74i	$⊢ (φ \to (φ \to ψ)) \leftrightarrow (φ \to ψ)$