Theorem or1 96

Description: Disjunction with 1.

Assertion

Ref	Expression
or1	(a ∪ 1) = 1

Proof of Theorem or1

Step	Hyp	Ref	Expression
1		df-t 40	. . . 4 1 = (a ∪ a⊥ )
2	1	lor 66	. . 3 (a ∪ 1) = (a ∪ (a ∪ a⊥ ))
3		ax-a4 32	. . 3 (a ∪ (a ∪ a⊥ )) = (a ∪ a⊥ )
4	2, 3	ax-r2 35	. 2 (a ∪ 1) = (a ∪ a⊥ )
5	1	ax-r1 34	. 2 (a ∪ a⊥ ) = 1
6	4, 5	ax-r2 35	1 (a ∪ 1) = 1

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

This theorem is referenced by:  or1r 97  an0 100  le1 138  sklem 222  0i1 265  wle1 371  ska2 414  woml6 418  oml6 470  i3con 533  ud1lem3 544  ud3lem1c 550  ud3lem3 558  ud4lem1c 561  ud4lem1 563  ud4lem3b 566  ud5lem1 571  u1lemoa 602  u4lemoa 605  u2lemonb 618  u3lemonb 619  u4lem5 746  u4lem6 750  u1lem11 762  u3lem8 765  u3lem11 768  test 784  2oalem1 807  oa6v4v 913

This theorem was proved from axioms:  ax-a2 30  ax-a4 32  ax-r1 34  ax-r2 35  ax-r5 37

This theorem depends on definitions:  df-t 40

metamath.org