Theorem comcom4 455

Description: Commutation equivalence. Kalmbach 83 p. 23.

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 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

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

Copyright terms: Public domain