Theorem comanr1 446

Description: Commutation law.

Assertion

Ref	Expression
comanr1	a C (a ^ b)

Proof of Theorem comanr1

Step	Hyp	Ref	Expression
1		coman1 177	. 2 (a ^ b) C a
2	1	comcom 435	1 a C (a ^ b)

Syntax hints:   C wc 3   ^ wa 7

This theorem is referenced by:  combi 467  ud3lem1a 548  ud5lem3a 573  ud5lem3b 574  ud5lem3 576  u1lemaa 582  u3lemaa 584  u4lemaa 585  u5lemaa 586  u3lemana 589  u4lemana 590  u5lemana 591  u1lemc1 662  u5lemc1 666  u4lemle2 700  u5lemle2 701  u21lembi 709  u4lem1 719  u4lem4 741  u24lem 752  u1lem11 762  u3lem10 767  u3lem13a 771  u3lem13b 772  bi1o1a 780  i1abs 783  3vth9 794  mlalem 814  bi3 821  bi4 822  imp3 823  mlaconj4 826  comanblem1 852  comanblem2 853  oas 905

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org