Theorem lecom 180

Description: Comparable elements commute. Beran 84 2.3(iii) p. 40.

Hypothesis

Ref	Expression
lecom.1	a =< b

Assertion

Ref	Expression
lecom	a C b

Proof of Theorem lecom

Step	Hyp	Ref	Expression
1		a5b 120	. . . 4 (a v (a ^ b')) = a
2	1	ax-r1 35	. . 3 a = (a v (a ^ b'))
3		lecom.1	. . . . . 6 a =< b
4	3	df2le2 136	. . . . 5 (a ^ b) = a
5	4	ax-r1 35	. . . 4 a = (a ^ b)
6	5	ax-r5 38	. . 3 (a v (a ^ b')) = ((a ^ b) v (a ^ b'))
7	2, 6	ax-r2 36	. 2 a = ((a ^ b) v (a ^ b'))
8	7	df-c1 132	1 a C b

Syntax hints:   =< wle 2   C wc 3  'wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  comorr 184  coman1 185  gsth 489  gt1 492  i3bi 496  oi3ai3 503  lem4 511  u1lemc6 706  comi12 707  u1lemle1 710  u2lemle1 711  u3lemle1 712  u4lemle1 713  u5lemle1 714  u12lembi 726  u3lem15 795  bi1o1a 798  3vcom 813  3vded21 817  1oa 820  2oalem1 825  mlalem 832  bi3 839  bi4 840  orbi 842  negantlem1 848  elimconslem 867  elimcons 868  comanblem1 870  mhlemlem1 874  mhlem 876  marsdenlem3 882  marsdenlem4 883  mlaconjolem 885  mlaconjo 886  mhcor1 888  e2ast2 894  e2astlem1 895  govar 896  gomaex3lem1 914  gomaex3lem2 915  oa3to4lem1 945  oa3to4lem2 946  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  oacom2 1012  lem4.6.2e1 1079  lem4.6.6i1j3 1091  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-le2 131  df-c1 132

Copyright terms: Public domain