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 3126  preqsn 3195  suceloni 3913  tz7.48lem 5371  msq0i 7452  prmdvdsexp 9739  pdivsq 14659  TTOid 15384  FFOid 15387  pm11.7 17567
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