![]() |
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 756 | . 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑) | |
2 | pm2.07 737 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑)) | |
3 | 1, 2 | impbii 126 | 1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∨ wo 708 |
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 709 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm4.25 758 orordi 773 orordir 774 truortru 1405 falorfal 1408 truxortru 1419 falxorfal 1422 unidm 3278 preqsn 3775 reapirr 8532 reapti 8534 lt2msq 8841 nn0ge2m1nn 9234 absext 11067 prmdvdsexp 12142 sqpweven 12169 2sqpwodd 12170 |
Copyright terms: Public domain | W3C validator |