Theorem orabs

Description: Absorption of redundant internal disjunct. Compare Theorem *4.45 of WhiteheadRussell p. 119. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 28-Feb-2014)

	Ref	Expression
Assertion	orabs	⊢ ( 𝜑 ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜑 ) )

Proof

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