Theorem comanr1 464

Description: Commutation law. (Contributed by NM, 26-Nov-1997.)

Assertion

Ref	Expression
comanr1	a C (a ∩ b)

Proof of Theorem comanr1

Step	Hyp	Ref	Expression
1		coman1 185	. 2 (a ∩ b) C a
2	1	comcom 453	1 a C (a ∩ b)

Syntax hints:   C wc 3   ∩ wa 7

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  combi  485  ud3lem1a  566  ud5lem3a  591  ud5lem3b  592  ud5lem3  594  u1lemaa  600  u3lemaa  602  u4lemaa  603  u5lemaa  604  u3lemana  607  u4lemana  608  u5lemana  609  u1lemc1  680  u5lemc1  684  u4lemle2  718  u5lemle2  719  u21lembi  727  u4lem1  737  u4lem4  759  u24lem  770  u1lem11  780  u3lem10  785  u3lem13a  789  u3lem13b  790  bi1o1a  798  i1abs  801  3vth9  812  mlalem  832  bi3  839  bi4  840  imp3  841  mlaconj4  844  comanblem1  870  comanblem2  871  oas  925