Theorem an1r 107

Description: Conjunction with 1.

Assertion

Ref	Expression
an1r	(1 ∩ a) = a

Proof of Theorem an1r

Step	Hyp	Ref	Expression
1		ancom 74	. 2 (1 ∩ a) = (a ∩ 1)
2		an1 106	. 2 (a ∩ 1) = a
3	1, 2	ax-r2 36	1 (1 ∩ a) = a

Syntax hints:   = wb 1   ∩ wa 7  1wt 8

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:  ud3lem1c  568  ud3lem3  576  ud5lem1  589  i2i1i1  800  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  lem3.3.7i2e1  1063  lem3.3.7i2e2  1064  lem3.3.7i3e2  1067  lem3.3.7i4e2  1070  lem4.6.6i1j3  1092  dp15lema  1152  xdp15  1197  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206