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

Theorem oridm 517
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 516 . 2 |- ((ph \/ ph) -> ph)
2 pm2.07 405 . 2 |- (ph -> (ph \/ ph))
31, 2impbii 188 1 |- ((ph \/ ph) <-> ph)
Colors of variables: wff set class
Syntax hints:   <-> wb 184   \/ wo 376
This theorem is referenced by:  pm4.25 518  orordi 533  orordir 534  unidm 2797  r19.12sn 3137  preqsn 3206  suceloni 3922  tz7.48lem 5378  msq0i 7458  prmdvdsexp 9687  pdivsq 14467  TTOid 15192  FFOid 15195  pm11.7 17416
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 185  df-or 378
Copyright terms: Public domain