Theorem oridm 243

Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117.

Assertion

Ref	Expression
oridm	|- ((ph \/ ph) <-> ph)

Proof of Theorem oridm

Step	Hyp	Ref	Expression
1		df-or 224	. 2 |- ((ph \/ ph) <-> (-. ph -> ph))
2		pm2.24 79	. . 3 |- (ph -> (-. ph -> ph))
3		pm2.18 81	. . 3 |- ((-. ph -> ph) -> ph)
4	2, 3	impbi 157	. 2 |- (ph <-> (-. ph -> ph))
5	1, 4	bitr4 176	1 |- ((ph \/ ph) <-> ph)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222

This theorem is referenced by:  pm4.25 244  pm1.2 245  orordi 266  orordir 267  unidm 2165  elsncg 2420  r19.12sn 2434  preqsn 2477  ordtri3or 2969  suceloni 3052  tz7.48lem 3940  msq0 5664  ismsg 7739  sinperlem2 8606

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

This theorem depends on definitions:  df-bi 147  df-or 224

Copyright terms: Public domain