![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > oridm | GIF version |
Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-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 757 | . 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑) | |
2 | pm2.07 738 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑)) | |
3 | 1, 2 | impbii 126 | 1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∨ wo 709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm4.25 759 orordi 774 orordir 775 truortru 1416 falorfal 1419 truxortru 1430 falxorfal 1433 unidm 3293 preqsn 3790 reapirr 8565 reapti 8567 lt2msq 8874 nn0ge2m1nn 9267 absext 11107 prmdvdsexp 12183 sqpweven 12210 2sqpwodd 12211 |
Copyright terms: Public domain | W3C validator |