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 2781  preqsn 3216  suceloni 3951  tz7.48lem 5557  msq0i 7726  prmdvdsexp 10193  pdivsq 17030  TTOid 17752  FFOid 17755  pm11.7 21433
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