Theorem lecom 172

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 112	. . . 4 (a v (a ^ b_|_)) = a
2	1	ax-r1 34	. . 3 a = (a v (a ^ b_|_))
3		lecom.1	. . . . . 6 a =< b
4	3	df2le2 128	. . . . 5 (a ^ b) = a
5	4	ax-r1 34	. . . 4 a = (a ^ b)
6	5	ax-r5 37	. . 3 (a v (a ^ b_|_)) = ((a ^ b) v (a ^ b_|_))
7	2, 6	ax-r2 35	. 2 a = ((a ^ b) v (a ^ b_|_))
8	7	df-c1 124	1 a C b

Syntax hints:   =< wle 2   C wc 3  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  comorr 176  coman1 177  gsth 471  gt1 474  i3bi 478  oi3ai3 485  lem4 493  u1lemc6 688  comi12 689  u1lemle1 692  u2lemle1 693  u3lemle1 694  u4lemle1 695  u5lemle1 696  u12lembi 708  u3lem15 777  bi1o1a 780  3vcom 795  3vded21 799  1oa 802  2oalem1 807  mlalem 814  bi3 821  bi4 822  orbi 824  negantlem1 830  elimconslem 849  elimcons 850  comanblem1 852  mhlemlem1 856  mhlem 858  marsdenlem3 864  marsdenlem4 865  mlaconjolem 867  mlaconjo 868  mhcor1 870  govar 876  gomaex3lem1 894  gomaex3lem2 895  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oacom2 992

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-le2 123  df-c1 124

metamath.org