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

Theorem oridm 495
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 494 . 2
2 pm2.07 383 . 2
31, 2impbii 178 1
Colors of variables: wff set class
Syntax hints:   wb 174   wo 356
This theorem is referenced by:  pm4.25 496  orordi 511  orordir 512  unidm 2778  r19.12sn 3133  preqsn 3207  suceloni 3938  tz7.48lem 5520  msq0i 7674  prmdvdsexp 10042  pdivsq 16714  TTOid 17438  FFOid 17441  pm11.7 20735
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 358
Copyright terms: Public domain