![]() |
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 903 | . 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑) | |
2 | pm2.07 902 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑)) | |
3 | 1, 2 | impbii 208 | 1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 846 |
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 206 df-or 847 |
This theorem is referenced by: pm4.25 905 orordi 928 orordir 929 nornot 1533 truortru 1579 falorfal 1582 unidm 4117 dfsn2ALT 4611 preqsnd 4821 sucexeloniOLD 7750 suceloniOLD 7752 tz7.48lem 8392 msq0i 11809 msq0d 11811 prmdvdsexp 16598 prmdvdssqOLD 16602 metn0 23729 rrxcph 24772 nb3grprlem2 28371 pm11.7 42750 euoreqb 45415 |
Copyright terms: Public domain | W3C validator |