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  5891  reapirr  8907  reapti  8909  lt2msq  9218  nn0ge2m1nn  9631  absext  11843  prmdvdsexp  12943  sqpweven  12971  2sqpwodd  12972