Theorem comcom7 442

Description: Commutation equivalence. Kalmbach 83 p. 23.

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

Syntax hints:   C wc 3  ^⊥ wn 4

This theorem is referenced by:  oml6 470  gsth2 472  gt1 474  dfi3b 481  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1d 551  ud3lem1 552  ud3lem3d 557  ud3lem3 558  ud5lem1b 569  ud5lem1 571  ud5lem3a 573  ud5lem3 576  u2lemaa 583  u2lemana 588  u4lemana 590  u3lemab 594  u3lemanb 599  u4lemoa 605  u4lemona 610  u3lemob 614  u3lemonb 619  comi12 689  u2lemle2 698  u4lemle2 700  u2lembi 703  u4lem5 746  u4lem6 750  u1lem11 762  u3lem11 768  u3lem13b 772  bi1o1a 780  test 784  mlalem 814  bi3 821  bi4 822  orbi 824  mlaconj4 826  neg3antlem2 847  elimconslem 849  mhlemlem1 856  mhlem 858  marsdenlem3 864  marsdenlem4 865  mlaconjo 868  mhcor1 870  govar 876

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