![]() |
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 3280 preqsn 3777 reapirr 8536 reapti 8538 lt2msq 8845 nn0ge2m1nn 9238 absext 11074 prmdvdsexp 12150 sqpweven 12177 2sqpwodd 12178 |
Copyright terms: Public domain | W3C validator |