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

Theorem oridm 747
 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 746 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 727 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 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  1384  falorfal  1387  truxortru  1398  falxorfal  1401  unidm  3225  preqsn  3711  reapirr  8383  reapti  8385  lt2msq  8688  nn0ge2m1nn  9081  absext  10887  prmdvdsexp  11882  sqpweven  11909  2sqpwodd  11910
 Copyright terms: Public domain W3C validator