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

Theorem oridm 904
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 903 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 902 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 208 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wo 846
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 206  df-or 847
This theorem is referenced by:  pm4.25  905  orordi  928  orordir  929  nornot  1533  truortru  1579  falorfal  1582  unidm  4117  dfsn2ALT  4611  preqsnd  4821  sucexeloniOLD  7750  suceloniOLD  7752  tz7.48lem  8392  msq0i  11809  msq0d  11811  prmdvdsexp  16598  prmdvdssqOLD  16602  metn0  23729  rrxcph  24772  nb3grprlem2  28371  pm11.7  42750  euoreqb  45415
  Copyright terms: Public domain W3C validator