Theorem comanr2 465

Description: Commutation law.

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

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