Theorem coman1 177

Description: Commutation law. Does not use OML.

Assertion

Ref	Expression
coman1	(a ∩ b) C a

Proof of Theorem coman1

Step	Hyp	Ref	Expression
1		lea 152	. 2 (a ∩ b) ≤ a
2	1	lecom 172	1 (a ∩ b) C a

Syntax hints:   C wc 3   ∩ wa 7

This theorem is referenced by:  coman2 178  comanr1 446  oml4 469  gsth2 472  i3bi 478  df2i3 480  dfi3b 481  oi3ai3 485  i3lem1 486  comi31 490  i3con 533  ud1lem1 542  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  u1lemle2 697  u2lemle2 698  u1lembi 702  u2lembi 703  u1lem4 739  u4lem6 750  u1lem8 758  u3lem11 768  u3lem13b 772  test 784  1oa 802  2oath1 808  oale 811  mlalem 814  bi3 821  mlaconj4 826  neg3antlem2 847  comanblem1 852  cancellem 873  govar 876  gomaex3lem3 896

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

metamath.org