Theorem comanr1 464

Description: Commutation law.

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 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

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

Copyright terms: Public domain