ILE Home 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  1339  falorfal  1342  truxortru  1353  falxorfal  1356  unidm  3132  preqsn  3604  reapirr  7998  reapti  8000  lt2msq  8285  nn0ge2m1nn  8669  absext  10395  prmdvdsexp  11033  sqpweven  11059  2sqpwodd  11060
  Copyright terms: Public domain W3C validator