Metamath Proof Explorer


Theorem oridm

Description: Idempotent law for disjunction. Theorem *4.25 of WhiteheadRussell p. 117. (Contributed by NM, 11-May-1993) (Proof shortened by Andrew Salmon, 16-Apr-2011) (Proof shortened by Wolf Lammen, 10-Mar-2013)

Ref Expression
Assertion oridm
|- ( ( ph \/ ph ) <-> ph )

Proof

Step Hyp Ref Expression
1 pm1.2
 |-  ( ( ph \/ ph ) -> ph )
2 pm2.07
 |-  ( ph -> ( ph \/ ph ) )
3 1 2 impbii
 |-  ( ( ph \/ ph ) <-> ph )