MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oridm Structured version   Visualization version   GIF version

Theorem oridm 905
Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-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 904 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 903 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 209 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wo 848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 207  df-or 849
This theorem is referenced by:  pm4.25  906  orordi  929  orordir  930  nornot  1531  truortru  1577  falorfal  1580  unidm  4157  dfsn2ALT  4647  preqsnd  4859  sucexeloniOLD  7830  suceloniOLD  7832  tz7.48lem  8481  msq0i  11910  msq0d  11912  prmdvdsexp  16752  metn0  24370  rrxcph  25426  nb3grprlem2  29398  pm11.7  44415  euoreqb  47121
  Copyright terms: Public domain W3C validator