Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  oridm GIF version

Theorem oridm 707
 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.)
Assertion
Ref Expression
oridm ((𝜑𝜑) ↔ 𝜑)

Proof of Theorem oridm
StepHypRef Expression
1 pm1.2 706 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 689 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 124 1 ((𝜑𝜑) ↔ 𝜑)
 Colors of variables: wff set class Syntax hints:   ↔ wb 103   ∨ wo 662 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  pm4.25  708  orordi  723  orordir  724  truortru  1337  falorfal  1340  truxortru  1351  falxorfal  1354  unidm  3116  preqsn  3575  reapirr  7744  reapti  7746  lt2msq  8031  nn0ge2m1nn  8415  absext  10087  prmdvdsexp  10671  sqpweven  10697  2sqpwodd  10698
 Copyright terms: Public domain W3C validator