Theorem or1 104

Description: Disjunction with 1. (Contributed by NM, 10-Aug-1997.)

Assertion

Ref	Expression
or1	(a ∪ 1) = 1

Proof of Theorem or1

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

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6  1wt 8

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

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  1057  lem3.3.7i3e2  1067