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

Theorem oridm 494
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 493 . 2
2 pm2.07 382 . 2
31, 2impbii 177 1
Colors of variables: wff set class
Syntax hints:   wb 173   wo 355
This theorem is referenced by:  pm4.25 495  orordi 510  orordir 511  unidm 2772  r19.12sn 3121  preqsn 3191  suceloni 3912  tz7.48lem 5446  msq0i 7567  prmdvdsexp 9877  pdivsq 15601  TTOid 16326  FFOid 16329  pm11.7 19414
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 174  df-or 357
Copyright terms: Public domain