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

Theorem oridm 496
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 495 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 383 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 178 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 174    \/ wo 356
This theorem is referenced by:  pm4.25  497  orordi  512  orordir  513  truortru  1284  falorfal  1287  unidm  2957  preqsn  3408  suceloni  4190  tz7.48lem  5900  msq0i  8613  prmdvdsexp  11279  metn0  15648  pdivsq  20690  pm11.7  24156
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 358
Copyright terms: Public domain