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

Theorem oridm 503
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 502 . 2 |- ((ph \/ ph) -> ph)
2 pm2.07 389 . 2 |- (ph -> (ph \/ ph))
31, 2impbii 178 1 |- ((ph \/ ph) <-> ph)
Colors of variables: wff set class
Syntax hints:   <-> wb 174   \/ wo 360
This theorem is referenced by:  pm4.25 504  orordi 519  orordir 520  unidm 2782  r19.12sn 3127  preqsn 3196  suceloni 3914  tz7.48lem 5386  msq0i 7467  prmdvdsexp 9756  pdivsq 14681  TTOid 15406  FFOid 15409  pm11.7 17589
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 362
Copyright terms: Public domain