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 746 | . 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑) | |
2 | pm2.07 727 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑)) | |
3 | 1, 2 | impbii 125 | 1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 698 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm4.25 748 orordi 763 orordir 764 truortru 1394 falorfal 1397 truxortru 1408 falxorfal 1411 unidm 3260 preqsn 3749 reapirr 8466 reapti 8468 lt2msq 8772 nn0ge2m1nn 9165 absext 10991 prmdvdsexp 12059 sqpweven 12086 2sqpwodd 12087 |
Copyright terms: Public domain | W3C validator |