Theorem comcom3 454

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

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 453	. . 3 b C a
3	2	comcom2 183	. 2 b C a⊥
4	3	comcom 453	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:  comcom4  455  comcom7  460  fh2  470  com2or  483  comcmtr1  494  i3lem1  504  lem4  511  i3abs3  524  i3con  551  ud1lem2  561  ud3lem1a  566  ud3lem1c  568  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud5lem1a  586  u4lemaa  603  u3lemana  607  u4lemana  608  u5lemana  609  u2lemanb  616  u3lemanb  617  u4lemanb  618  u5lemanb  619  u2lemc4  702  u3lemc4  703  u4lemc4  704  u5lemc4  705  u4lemle2  718  u21lembi  727  u4lem1  737  u2lem3  750  u4lem4  759  u5lem5  765  u4lem6  768  u5lem6  769  u1lem11  780  u3lem8  783  u3lem10  785  u3lem13a  789  u3lem13b  790  3vded3  819  1oa  820  mlalem  832  bi3  839  bi4  840  imp3  841  mlaconj4  844  elimcons  868  comanblem1  870  mhlem1  877  mhlem2  878  marsdenlem1  880  marsdenlem2  881  oa3to4lem1  945  oa3to4lem2  946  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  lem4.6.7  1103