|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > oridm | Structured version Visualization version GIF version | ||
| 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 | 
|---|---|
| oridm | ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | pm1.2 904 | . 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑) | |
| 2 | pm2.07 903 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑)) | |
| 3 | 1, 2 | impbii 209 | 1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∨ wo 848 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 | 
| This theorem depends on definitions: df-bi 207 df-or 849 | 
| This theorem is referenced by: pm4.25 906 orordi 929 orordir 930 nornot 1531 truortru 1577 falorfal 1580 unidm 4157 dfsn2ALT 4647 preqsnd 4859 sucexeloniOLD 7830 suceloniOLD 7832 tz7.48lem 8481 msq0i 11910 msq0d 11912 prmdvdsexp 16752 metn0 24370 rrxcph 25426 nb3grprlem2 29398 pm11.7 44415 euoreqb 47121 | 
| Copyright terms: Public domain | W3C validator |