ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  oridm Unicode version

Theorem oridm 752
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 751 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 732 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 125 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm4.25  753  orordi  768  orordir  769  truortru  1400  falorfal  1403  truxortru  1414  falxorfal  1417  unidm  3270  preqsn  3760  reapirr  8489  reapti  8491  lt2msq  8795  nn0ge2m1nn  9188  absext  11020  prmdvdsexp  12095  sqpweven  12122  2sqpwodd  12123
  Copyright terms: Public domain W3C validator