Theorem oridm 514

Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.)

Assertion

Ref	Expression
oridm

Proof of Theorem oridm

Step	Hyp	Ref	Expression
1		pm1.2 513	. 2
2		pm2.07 396	. 2
3	1, 2	impbii 188	1

Syntax hints:  <->wb 184  \/wo 368

This theorem is referenced by:  pm4.25  515  orordi  530  orordir  531  truortru  1423  falorfal  1426  unidm  3646  preqsn  4213  suceloni  6648  tz7.48lem  7125  msq0i  10221  msq0d  10223  prmdvdsexp  14255  metn0  20863  rrxcph  21824  nb3graprlem2  24452  preqsnd  27418  pdivsq  29174  nofulllem5  29466  pm11.7  31302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-or 370