Theorem oridm 706

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 705	. 2 |- ( ( ph \/ ph ) -> ph )
2		pm2.07 688	. 2 |- ( ph -> ( ph \/ ph ) )
3	1, 2	impbii 124	1 |- ( ( ph \/ ph ) <-> ph )

Syntax hints:   <-> wb 103   \/ wo 661

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm4.25  707  orordi  722  orordir  723  truortru  1336  falorfal  1339  truxortru  1350  falxorfal  1353  unidm  3115  preqsn  3567  reapirr  7677  reapti  7679  lt2msq  7964  nn0ge2m1nn  8348  absext  9949  prmdvdsexp  10527  sqpweven  10553  2sqpwodd  10554