Theorem comcom4 437

Description: Commutation equivalence. Kalmbach 83 p. 23.

Hypothesis

Ref	Expression
comcom.1	a C b

Assertion

Ref	Expression
comcom4	a⊥ C b⊥

Proof of Theorem comcom4

Step	Hyp	Ref	Expression
1		comcom.1	. . 3 a C b
2	1	comcom3 436	. 2 a⊥ C b
3	2	comcom2 175	1 a⊥ C b⊥

Syntax hints:   C wc 3  ^⊥ wn 4

This theorem is referenced by:  comd 438  comcom5 440  fh3 453  fh4 454  com2an 466  gstho 473  i3abs3 506  u2lemc4 684  u3lemc4 685  u4lemc4 686  u5lemc4 687  u2lem3 732  u4lem4 741  u5lem5 747  u5lem6 751  3vded3 801  marsdenlem1 862  marsdenlem2 863

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