Theorem or1 98

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 67	. . 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 99  an0 102  le1 140  sklem 224  0i1 267  wle1 375  ska2 418  woml6 422  oml6 474  i3con 537  ud1lem3 548  ud3lem1c 554  ud3lem3 562  ud4lem1c 565  ud4lem1 567  ud4lem3b 570  ud5lem1 575  u1lemoa 606  u4lemoa 609  u2lemonb 622  u3lemonb 623  u4lem5 750  u4lem6 754  u1lem11 766  u3lem8 769  u3lem11 772  test 788  2oalem1 811  oa6v4v 919  lem3.3.7i0e1 1042  lem3.3.7i3e2 1052

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