Theorem comid 187

Description: Identity law for commutation. Does not use OML.

Assertion

Ref	Expression
comid	a C a

Proof of Theorem comid

Step	Hyp	Ref	Expression
1		comorr 184	. 2 a C (a v a)
2		oridm 110	. 2 (a v a) = a
3	1, 2	cbtr 182	1 a C a

Syntax hints:   C wc 3   v wo 6

This theorem is referenced by:  comi32 510  i3abs3 524  ud1lem2 561  ud1lem3 562  ud2lem3 565  ud4lem2 582  ud4lem3 585  u1lemaa 600  u3lemaa 602  u3lemana 607  u2lemanb 616  u4lemanb 618  u4lemob 633  u1lemc1 680  u2lemc1 681  u4lemc1 683  u1lemc3 691  u2lemc5 697  u4lemc5 699  u1lemc4 701  u3lemc4 703  u4lemc4 704  u5lemc4 705  u3lem2 746  u1lem4 757  u4lem4 759  u3lem13a 789  bi1o1a 798  3vded21 817  3vded3 819  1oa 820  mhlem1 877  marsdenlem2 881  gomaex3lem1 914  gomaex3lem2 915  gomaex3lem3 916  oa3to4lem1 945  oa3to4lem2 946  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  com3iia 1099  lem4.6.7 1100

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  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