Theorem comcom3 436

Description: Commutation equivalence. Kalmbach 83 p. 23.

Hypothesis

Ref	Expression
comcom.1	a C b

Assertion

Ref	Expression
comcom3	a⊥ C b

Proof of Theorem comcom3

Step	Hyp	Ref	Expression
1		comcom.1	. . . 4 a C b
2	1	comcom 435	. . 3 b C a
3	2	comcom2 175	. 2 b C a⊥
4	3	comcom 435	1 a⊥ C b

Syntax hints:   C wc 3  ^⊥ wn 4

This theorem is referenced by:  comcom4 437  comcom7 442  fh2 452  com2or 465  comcmtr1 476  i3lem1 486  lem4 493  i3abs3 506  i3con 533  ud1lem2 543  ud3lem1a 548  ud3lem1c 550  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud5lem1a 568  u4lemaa 585  u3lemana 589  u4lemana 590  u5lemana 591  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u2lemc4 684  u3lemc4 685  u4lemc4 686  u5lemc4 687  u4lemle2 700  u21lembi 709  u4lem1 719  u2lem3 732  u4lem4 741  u5lem5 747  u4lem6 750  u5lem6 751  u1lem11 762  u3lem8 765  u3lem10 767  u3lem13a 771  u3lem13b 772  3vded3 801  1oa 802  mlalem 814  bi3 821  bi4 822  imp3 823  mlaconj4 826  elimcons 850  comanblem1 852  mhlem1 859  mhlem2 860  marsdenlem1 862  marsdenlem2 863  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942

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