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 5342  msq0i 7418  pdivsq 13869  TTOid 14594  FFOid 14597  pm11.7 16830
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