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 2802  r19.12sn 3140  preqsn 3209  suceloni 3918  tz7.48lem 5344  msq0i 7421  prmdvdsexp 9652  pdivsq 14023  TTOid 14748  FFOid 14751  pm11.7 16981
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