![]() |
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 714 | . 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑) | |
2 | pm2.07 697 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑)) | |
3 | 1, 2 | impbii 125 | 1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 670 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm4.25 716 orordi 731 orordir 732 truortru 1351 falorfal 1354 truxortru 1365 falxorfal 1368 unidm 3166 preqsn 3649 reapirr 8205 reapti 8207 lt2msq 8502 nn0ge2m1nn 8889 absext 10675 prmdvdsexp 11619 sqpweven 11645 2sqpwodd 11646 |
Copyright terms: Public domain | W3C validator |