Theorem oridm 769

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 768	. 2 |- ( ( ph \/ ph ) -> ph )
2		pm2.07 749	. 2 |- ( ph -> ( ph \/ ph ) )
3	1, 2	impbii 126	1 |- ( ( ph \/ ph ) <-> ph )

This proof depends on syntax axioms:   <-> wb 105   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.25  770  orordi  785  orordir  786  truortru  1454  falorfal  1457  truxortru  1468  falxorfal  1471  unidm  3372  preqsn  3900  funopsn  5894  reapirr  8913  reapti  8915  lt2msq  9224  nn0ge2m1nn  9638  absext  11851  prmdvdsexp  12952  sqpweven  12980  2sqpwodd  12981