HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem oridm 499
Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (The proof was shortened by Andrew Salmon, 16-Apr-2011.) (The proof was shortened by Wolf Lammen, 10-Mar-2013.)
Assertion
Ref Expression
oridm

Proof of Theorem oridm
StepHypRef Expression
1 pm1.2 498 . 2
2 pm2.07 386 . 2
31, 2impbii 178 1
Colors of variables: wff set class
Syntax hints:   wb 174   wo 359
This theorem is referenced by:  pm4.25 500  orordi 515  orordir 516  unidm 2774  r19.12sn 3122  preqsn 3191  suceloni 3909  tz7.48lem 5385  msq0i 7466  prmdvdsexp 9758  pdivsq 14683  TTOid 15408  FFOid 15411  pm11.7 18240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 175  df-or 361
Copyright terms: Public domain