Theorem oridm 747

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

Step	Hyp	Ref	Expression
1		pm1.2 746	. 2 |- ( ( ph \/ ph ) -> ph )
2		pm2.07 727	. 2 |- ( ph -> ( ph \/ ph ) )
3	1, 2	impbii 125	1 |- ( ( ph \/ ph ) <-> ph )

Syntax hints:   <-> wb 104   \/ wo 698

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.25  748  orordi  763  orordir  764  truortru  1384  falorfal  1387  truxortru  1398  falxorfal  1401  unidm  3224  preqsn  3710  reapirr  8363  reapti  8365  lt2msq  8668  nn0ge2m1nn  9061  absext  10867  prmdvdsexp  11862  sqpweven  11889  2sqpwodd  11890