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 ∪ a)
2		oridm 110	. 2 (a ∪ a) = a
3	1, 2	cbtr 182	1 a C a

Syntax hints:   C wc 3   ∪ wo 6

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

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  1100  lem4.6.7  1101