Theorem comcom7 460

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

Hypothesis

Ref	Expression
comcom7.1	a C b⊥

Assertion

Ref	Expression
comcom7	a C b

Proof of Theorem comcom7

Step	Hyp	Ref	Expression
1		comcom7.1	. . 3 a C b⊥
2	1	comcom3 454	. 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:  oml6  488  gsth2  490  gt1  492  dfi3b  499  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem1d  569  ud3lem1  570  ud3lem3d  575  ud3lem3  576  ud5lem1b  587  ud5lem1  589  ud5lem3a  591  ud5lem3  594  u2lemaa  601  u2lemana  606  u4lemana  608  u3lemab  612  u3lemanb  617  u4lemoa  623  u4lemona  628  u3lemob  632  u3lemonb  637  comi12  707  u2lemle2  716  u4lemle2  718  u2lembi  721  u4lem5  764  u4lem6  768  u1lem11  780  u3lem11  786  u3lem13b  790  bi1o1a  798  test  802  mlalem  832  bi3  839  bi4  840  orbi  842  mlaconj4  844  neg3antlem2  865  elimconslem  867  mhlemlem1  874  mhlem  876  marsdenlem3  882  marsdenlem4  883  mlaconjo  886  mhcor1  888  e2astlem1  895  govar  896  oa3moa3  1029  lem4.6.2e1  1082