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

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

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  3219  preqsn  3702  reapirr  8339  reapti  8341  lt2msq  8644  nn0ge2m1nn  9037  absext  10835  prmdvdsexp  11826  sqpweven  11853  2sqpwodd  11854