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	$$⊢\left(\phi \to \left(\phi \to \psi \right)\right)\leftrightarrow \left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		pm5.5	$$⊢\phi \to \left(\left(\phi \to \psi \right)\leftrightarrow \psi \right)$$
2	1	pm5.74i	$$⊢\left(\phi \to \left(\phi \to \psi \right)\right)\leftrightarrow \left(\phi \to \psi \right)$$