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

Theorem oridm 523
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 |- ((ph \/ ph) <-> ph)

Proof of Theorem oridm
StepHypRef Expression
1 pm1.2 522 . 2 |- ((ph \/ ph) -> ph)
2 pm2.07 410 . 2 |- (ph -> (ph \/ ph))
31, 2impbii 193 1 |- ((ph \/ ph) <-> ph)
Colors of variables: wff set class
Syntax hints:   <-> wb 189   \/ wo 381
This theorem is referenced by:  pm4.25 524  orordi 539  orordir 540  unidm 2803  r19.12sn 3143  preqsn 3212  suceloni 3926  tz7.48lem 5381  msq0i 7458  prmdvdsexp 9671  pdivsq 14270  TTOid 14995  FFOid 14998  pm11.7 17221
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 190  df-or 383
Copyright terms: Public domain