Theorem an1 106

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

Assertion

Ref	Expression
an1	(a ∩ 1) = a

Proof of Theorem an1

Step	Hyp	Ref	Expression
1		df-a 40	. 2 (a ∩ 1) = (a⊥ ∪ 1⊥ )⊥
2		df-f 42	. . . . . 6 0 = 1⊥
3	2	ax-r1 35	. . . . 5 1⊥ = 0
4	3	lor 70	. . . 4 (a⊥ ∪ 1⊥ ) = (a⊥ ∪ 0)
5		or0 102	. . . 4 (a⊥ ∪ 0) = a⊥
6	4, 5	ax-r2 36	. . 3 (a⊥ ∪ 1⊥ ) = a⊥
7	6	con2 67	. 2 (a⊥ ∪ 1⊥ )⊥ = a
8	1, 7	ax-r2 36	1 (a ∩ 1) = a

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

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

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

This theorem is referenced by:  an1r  107  1b  117  comm0  178  comm1  179  lei3  246  i3id  251  1i1  274  wql2lem5  292  wlem14  430  ska4  433  woml6  436  oml6  488  i3lem1  504  i3le  515  i3abs3  524  i3con  551  ud1lem1  560  ud1lem2  561  ud1lem3  562  ud2lem3  565  ud3lem1c  568  ud3lem1  570  ud3lem3  576  ud4lem1c  579  ud4lem1  581  ud4lem2  582  ud4lem3b  584  ud4lem3  585  ud5lem1  589  ud5lem3  594  u4lemoa  623  u4lemona  628  u3lemob  632  u4lemob  633  u3lemonb  637  u1lemc4  701  u2lemc4  702  u3lemc4  703  u4lemc4  704  u5lemc4  705  u1lemle2  715  u2lemle2  716  u4lemle2  718  u5lemle2  719  oi3oa3  733  u2lem3  750  u3lem3  751  u1lem4  757  u4lem4  759  u4lem5  764  u5lem5  765  u4lem6  768  u5lem6  769  u1lem11  780  u3lem10  785  u3lem11  786  u3lem13a  789  u3lem13b  790  u3lem14a  791  i1abs  801  test  802  test2  803  3vded12  815  3vded13  816  3vded3  819  3vroa  831  negantlem2  849  neg3antlem2  865  elimconslem  867  elimcons  868  mhlem1  877  oago3.29  889  gomaex3lem1  914  gomaex3lem2  915  gomaex3lem3  916  gomaex3lem7  920  oau  929  oa6v4v  933  oa23  936  oa3to4lem1  945  oa3to4lem2  946  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa3-2lema  978  oa3-2lemb  979  oa3-6lem  980  oa3-3lem  981  oa3-1lem  982  oa3-4lem  983  oa3-5lem  984  oa3-u1lem  985  oa3-u2lem  986  oa3-6to3  987  oa3-2to4  988  oa3-2to2s  990  oa3-u1  991  oa3-u2  992  lem3.3.7i0e1  1057  lem3.3.7i1e2  1061  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070