Theorem comcom6 459

Description: Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 26-Nov-1997.)

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 183	. 2 a⊥ C b⊥
3	2	comcom5 458	1 a C b

Syntax hints:   C wc 3  ^⊥ wn 4

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  combi  485  ud3lem1a  566  ud3lem1c  568  ud5lem3a  591  ud5lem3b  592  ud5lem3  594  u3lemaa  602  u4lemaa  603  u5lemaa  604  u3lemab  612  u4lemab  613  u5lemab  614  u2lemc1  681  u5lemc1  684  u5lemc1b  685  u1lemc6  706  u4lemle2  718  u5lemle2  719  u4lem5  764  u24lem  770  u3lem7  774  i1abs  801  3vth7  810  3vth9  812  3vcom  813  2oalem1  825  oale  829  bi4  840  negantlem1  848  elimconslem  867  comanblem2  871  mhlem1  877  marsdenlem2  881  oas  925  lem4.6.2e1  1082  lem4.6.6i1j3  1094