Theorem pm4.45

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

	Ref	Expression
Assertion	pm4.45	⊢ ( 𝜑 ↔ ( 𝜑 ∧ ( 𝜑 ∨ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		orc	⊢ ( 𝜑 → ( 𝜑 ∨ 𝜓 ) )
2	1	pm4.71i	⊢ ( 𝜑 ↔ ( 𝜑 ∧ ( 𝜑 ∨ 𝜓 ) ) )