Theorem coman1 185

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 160	. 2 (a ∩ b) ≤ a
2	1	lecom 180	1 (a ∩ b) C a

Syntax hints:   C wc 3   ∩ wa 7

This theorem is referenced by:  coman2 186  comanr1 464  oml4 487  gsth2 490  i3bi 496  df2i3 498  dfi3b 499  oi3ai3 503  i3lem1 504  comi31 508  i3con 551  ud1lem1 560  ud3lem1a 566  ud3lem1c 568  ud3lem1 570  ud3lem3d 575  ud3lem3 576  ud4lem1a 577  ud4lem1b 578  ud4lem1c 579  ud4lem1 581  ud5lem1a 586  ud5lem1b 587  ud5lem1 589  ud5lem3a 591  ud5lem3 594  u2lemaa 601  u2lemana 606  u1lemab 610  u3lemab 612  u1lemanb 615  u3lemanb 617  u1lemle2 715  u2lemle2 716  u1lembi 720  u2lembi 721  u1lem4 757  u4lem6 768  u1lem8 776  u3lem11 786  u3lem13b 790  test 802  1oa 820  2oath1 826  oale 829  mlalem 832  bi3 839  mlaconj4 844  neg3antlem2 865  comanblem1 870  cancellem 891  govar 896  gomaex3lem3 916  lem4.6.2e1 1079

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-le1 130  df-le2 131  df-c1 132

Copyright terms: Public domain