Theorem comanr2 465

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

Assertion

Ref	Expression
comanr2	b C (a ∩ b)

Proof of Theorem comanr2

Step	Hyp	Ref	Expression
1		coman2 186	. 2 (a ∩ b) C b
2	1	comcom 453	1 b 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:  ud3lem1a  566  u4lemaa  603  u4lemana  608  u3lemab  612  u4lemab  613  u5lemab  614  u2lemanb  616  u3lemanb  617  u4lemanb  618  u5lemanb  619  u2lemc1  681  u4lemc1  683  u5lemc1b  685  u4lemle2  718  u4lem5  764  u4lem6  768  u24lem  770  u3lem13b  790  3vth7  810  1oa  820  oale  829  mlalem  832  bi3  839  bi4  840  mhlem1  877