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

Theorem oridm 731
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 730 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 711 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 125 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104  wo 682
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 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm4.25  732  orordi  747  orordir  748  truortru  1368  falorfal  1371  truxortru  1382  falxorfal  1385  unidm  3189  preqsn  3672  reapirr  8307  reapti  8309  lt2msq  8612  nn0ge2m1nn  9005  absext  10803  prmdvdsexp  11753  sqpweven  11780  2sqpwodd  11781
  Copyright terms: Public domain W3C validator