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  3898  funopsn  5885  reapirr  8899  reapti  8901  lt2msq  9210  nn0ge2m1nn  9610  absext  11812  prmdvdsexp  12909  sqpweven  12936  2sqpwodd  12937