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