Theorem an1 98

Description: Conjunction with 1.

Assertion

Ref	Expression
an1	(a ∩ 1) = a

Proof of Theorem an1

Step	Hyp	Ref	Expression
1		df-a 39	. 2 (a ∩ 1) = (a⊥ ∪ 1⊥ )⊥
2		df-f 41	. . . . . 6 0 = 1⊥
3	2	ax-r1 34	. . . . 5 1⊥ = 0
4	3	lor 66	. . . 4 (a⊥ ∪ 1⊥ ) = (a⊥ ∪ 0)
5		or0 94	. . . 4 (a⊥ ∪ 0) = a⊥
6	4, 5	ax-r2 35	. . 3 (a⊥ ∪ 1⊥ ) = a⊥
7	6	con2 64	. 2 (a⊥ ∪ 1⊥ )⊥ = a
8	1, 7	ax-r2 35	1 (a ∩ 1) = a

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 9  0wf 10

This theorem is referenced by:  an1r 99  1b 109  comm0 170  comm1 171  lei3 238  i3id 243  1i1 266  wql2lem5 284  wlem14 412  ska2 414  ska4 415  woml6 418  oml6 470  i3lem1 486  i3le 497  i3abs3 506  i3con 533  ud1lem1 542  ud1lem2 543  ud1lem3 544  ud2lem3 547  ud3lem1c 550  ud3lem1 552  ud3lem3 558  ud4lem1c 561  ud4lem1 563  ud4lem2 564  ud4lem3b 566  ud4lem3 567  ud5lem1 571  ud5lem3 576  u4lemoa 605  u4lemona 610  u3lemob 614  u4lemob 615  u3lemonb 619  u1lemc4 683  u2lemc4 684  u3lemc4 685  u4lemc4 686  u5lemc4 687  u1lemle2 697  u2lemle2 698  u4lemle2 700  u5lemle2 701  oi3oa3 715  u2lem3 732  u3lem3 733  u1lem4 739  u4lem4 741  u4lem5 746  u5lem5 747  u4lem6 750  u5lem6 751  u1lem11 762  u3lem10 767  u3lem11 768  u3lem13a 771  u3lem13b 772  u3lem14a 773  i1abs 783  test 784  test2 785  3vded12 797  3vded13 798  3vded3 801  3vroa 813  negantlem2 831  neg3antlem2 847  elimconslem 849  elimcons 850  mhlem1 859  oago3.29 871  gomaex3lem1 894  gomaex3lem2 895  gomaex3lem3 896  gomaex3lem7 900  oau 909  oa6v4v 913  oa23 916  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa3-2lema 958  oa3-2lemb 959  oa3-6lem 960  oa3-3lem 961  oa3-1lem 962  oa3-4lem 963  oa3-5lem 964  oa3-u1lem 965  oa3-u2lem 966  oa3-6to3 967  oa3-2to4 968  oa3-2to2s 970  oa3-u1 971  oa3-u2 972

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-t 40  df-f 41

metamath.org