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

Theorem oridm 715
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 714 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 697 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 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