Theorem comcom6 441

Description: Commutation equivalence. Kalmbach 83 p. 23.

Hypothesis

Ref	Expression
comcom6.1	a_|_ C b

Assertion

Ref	Expression
comcom6	a C b

Proof of Theorem comcom6

Step	Hyp	Ref	Expression
1		comcom6.1	. . 3 a_|_ C b
2	1	comcom2 175	. 2 a_|_ C b_|_
3	2	comcom5 440	1 a C b

Syntax hints:   C wc 3  _|_wn 4

This theorem is referenced by:  combi 467  ud3lem1a 548  ud3lem1c 550  ud5lem3a 573  ud5lem3b 574  ud5lem3 576  u3lemaa 584  u4lemaa 585  u5lemaa 586  u3lemab 594  u4lemab 595  u5lemab 596  u2lemc1 663  u5lemc1 666  u5lemc1b 667  u1lemc6 688  u4lemle2 700  u5lemle2 701  u4lem5 746  u24lem 752  u3lem7 756  i1abs 783  3vth7 792  3vth9 794  3vcom 795  2oalem1 807  oale 811  bi4 822  negantlem1 830  elimconslem 849  comanblem2 853  mhlem1 859  marsdenlem2 863  oas 905

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org