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

Theorem oridm 746
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 745 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 726 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 125 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 697
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 698
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm4.25  747  orordi  762  orordir  763  truortru  1383  falorfal  1386  truxortru  1397  falxorfal  1400  unidm  3214  preqsn  3697  reapirr  8332  reapti  8334  lt2msq  8637  nn0ge2m1nn  9030  absext  10828  prmdvdsexp  11815  sqpweven  11842  2sqpwodd  11843
  Copyright terms: Public domain W3C validator