Theorem pm4.44

Description: Theorem *4.44 of WhiteheadRussell p. 119. (Contributed by NM, 3-Jan-2005)

	Ref	Expression
Assertion	pm4.44	$$⊢\phi \leftrightarrow \left(\phi \vee \left(\phi \wedge \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		orc	$$⊢\phi \to \left(\phi \vee \left(\phi \wedge \psi \right)\right)$$
2		id	$$⊢\phi \to \phi$$
3		simpl	$$⊢\left(\phi \wedge \psi \right)\to \phi$$
4	2 3	jaoi	$$⊢\left(\phi \vee \left(\phi \wedge \psi \right)\right)\to \phi$$
5	1 4	impbii	$$⊢\phi \leftrightarrow \left(\phi \vee \left(\phi \wedge \psi \right)\right)$$