Theorem coman2 178

Description: Commutation law. Does not use OML.

Assertion

Ref	Expression
coman2	(a ^ b) C b

Proof of Theorem coman2

Step	Hyp	Ref	Expression
1		ancom 68	. 2 (a ^ b) = (b ^ a)
2		coman1 177	. 2 (b ^ a) C b
3	1, 2	bctr 173	1 (a ^ b) C b

Syntax hints:   C wc 3   ^ wa 7

This theorem is referenced by:  comanr2 447  gsth 471  dfi3b 481  i3con 533  ud1lem1 542  ud2lem3 547  ud3lem1a 548  ud3lem1c 550  ud3lem1 552  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1 563  ud5lem1a 568  ud5lem1b 569  ud5lem1 571  ud5lem3a 573  ud5lem3 576  u2lemaa 583  u2lemana 588  u1lemab 592  u3lemab 594  u1lemanb 597  u3lemanb 599  u2lemle2 698  u1lembi 702  u2lembi 703  u1lem4 739  u4lem6 750  u1lem8 758  u3lem11 768  u3lem13b 772  1oa 802  mlalem 814  bi3 821  mlaconj4 826  neg3antlem2 847  comanblem1 852  cancellem 873  govar 876

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

This theorem depends on definitions:  df-a 39  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org