Theorem comanr2 447

Description: Commutation law.

Assertion

Ref	Expression
comanr2	b C (a ^ b)

Proof of Theorem comanr2

Step	Hyp	Ref	Expression
1		coman2 178	. 2 (a ^ b) C b
2	1	comcom 435	1 b C (a ^ b)

Syntax hints:   C wc 3   ^ wa 7

This theorem is referenced by:  ud3lem1a 548  u4lemaa 585  u4lemana 590  u3lemab 594  u4lemab 595  u5lemab 596  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u2lemc1 663  u4lemc1 665  u5lemc1b 667  u4lemle2 700  u4lem5 746  u4lem6 750  u24lem 752  u3lem13b 772  3vth7 792  1oa 802  oale 811  mlalem 814  bi3 821  bi4 822  mhlem1 859

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