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

Theorem oridm 493
Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.)
Assertion
Ref Expression
oridm  |-  ( (
ph  \/  ph )  <->  ph )

Proof of Theorem oridm
StepHypRef Expression
1 pm1.2 492 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 382 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 178 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 174    \/ wo 355
This theorem is referenced by:  pm4.25  494  orordi  509  orordir  510  truortru  1273  falorfal  1276  unidm  2938  preqsn  3392  suceloni  4169  tz7.48lem  5904  msq0i  8632  prmdvdsexp  11366  metn0  16074  pdivsq  21265  pm11.7  24708
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 357
Copyright terms: Public domain