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

Theorem oridm 581
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 580 . 2 |- ((ph \/ ph) -> ph)
2 pm2.07 447 . 2 |- (ph -> (ph \/ ph))
31, 2impbii 213 1 |- ((ph \/ ph) <-> ph)
Colors of variables: wff set class
Syntax hints:   <-> wb 209   \/ wo 417
This theorem is referenced by:  pm1.2OLD 582  pm4.25 584  orordi 599  orordir 600  unidm 2940  r19.12sn 3278  preqsn 3342  suceloni 4055  tz7.48lem 5482  msq0i 7556  sinperlem2 11562  TTOid 14569  FFOid 14572  pm11.7 16980
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 210  df-or 419
Copyright terms: Public domain