Theorem or1 104

Description: Disjunction with 1.

Assertion

Ref	Expression
or1	(a v 1) = 1

Proof of Theorem or1

Step	Hyp	Ref	Expression
1		df-t 41	. . . 4 1 = (a v a')
2	1	lor 70	. . 3 (a v 1) = (a v (a v a'))
3		ax-a4 33	. . 3 (a v (a v a')) = (a v a')
4	2, 3	ax-r2 36	. 2 (a v 1) = (a v a')
5	1	ax-r1 35	. 2 (a v a') = 1
6	4, 5	ax-r2 36	1 (a v 1) = 1

Syntax hints:   = wb 1  'wn 4   v wo 6  1wt 8

This theorem is referenced by:  or1r 105  an0 108  le1 146  sklem 230  0i1 273  wle1 389  ska2 432  woml6 436  oml6 488  i3con 551  ud1lem3 562  ud3lem1c 568  ud3lem3 576  ud4lem1c 579  ud4lem1 581  ud4lem3b 584  ud5lem1 589  u1lemoa 620  u4lemoa 623  u2lemonb 636  u3lemonb 637  u4lem5 764  u4lem6 768  u1lem11 780  u3lem8 783  u3lem11 786  test 802  2oalem1 825  oa6v4v 933  lem3.3.7i0e1 1056  lem3.3.7i3e2 1066

This theorem was proved from axioms:  ax-a2 31  ax-a4 33  ax-r1 35  ax-r2 36  ax-r5 38

This theorem depends on definitions:  df-t 41

Copyright terms: Public domain