Metamath Proof Explorer


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 φφψφ