Theorem an1r 107

Description: Conjunction with 1. (Contributed by NM, 26-Nov-1997.)

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:  ska2  432  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  1094  dp15lema  1154  xdp15  1199  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208