Theorem comcom3 454

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

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