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 2778  r19.12sn 3126  preqsn 3195  suceloni 3913  tz7.48lem 5398  msq0i 7482  prmdvdsexp 9776  pdivsq 15076  TTOid 15801  FFOid 15804  pm11.7 18762
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