Theorem comcom4 455

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

Hypothesis

Ref	Expression
comcom.1	a C b

Assertion

Ref	Expression
comcom4	a⊥ C b⊥

Proof of Theorem comcom4

Step	Hyp	Ref	Expression
1		comcom.1	. . 3 a C b
2	1	comcom3 454	. 2 a⊥ C b
3	2	comcom2 183	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:  comd  456  comcom5  458  fh3  471  fh4  472  com2an  484  gstho  491  i3abs3  524  u2lemc4  702  u3lemc4  703  u4lemc4  704  u5lemc4  705  u2lem3  750  u4lem4  759  u5lem5  765  u5lem6  769  3vded3  819  marsdenlem1  880  marsdenlem2  881