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

Theorem oridm 570
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 569 . 2 |- ((ph \/ ph) -> ph)
2 pm2.07 441 . 2 |- (ph -> (ph \/ ph))
31, 2impbii 207 1 |- ((ph \/ ph) <-> ph)
Colors of variables: wff set class
Syntax hints:   <-> wb 203   \/ wo 411
This theorem is referenced by:  pm4.25 571  orordi 586  orordir 587  unidm 2923  r19.12sn 3261  preqsn 3325  suceloni 4038  tz7.48lem 5465  msq0i 7539  sinperlem2 11598  pdivsq 14056  TTOid 14791  FFOid 14794  pm11.7 17202
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 204  df-or 413
Copyright terms: Public domain