Theorem comcom7 460

Description: Commutation equivalence. Kalmbach 83 p. 23.

Hypothesis

Ref	Expression
comcom7.1	a C b'

Assertion

Ref	Expression
comcom7	a C b

Proof of Theorem comcom7

Step	Hyp	Ref	Expression
1		comcom7.1	. . 3 a C b'
2	1	comcom3 454	. 2 a' C b'
3	2	comcom5 458	1 a C b

Syntax hints:   C wc 3  'wn 4

This theorem is referenced by:  oml6 488  gsth2 490  gt1 492  dfi3b 499  ud3lem1a 566  ud3lem1b 567  ud3lem1c 568  ud3lem1d 569  ud3lem1 570  ud3lem3d 575  ud3lem3 576  ud5lem1b 587  ud5lem1 589  ud5lem3a 591  ud5lem3 594  u2lemaa 601  u2lemana 606  u4lemana 608  u3lemab 612  u3lemanb 617  u4lemoa 623  u4lemona 628  u3lemob 632  u3lemonb 637  comi12 707  u2lemle2 716  u4lemle2 718  u2lembi 721  u4lem5 764  u4lem6 768  u1lem11 780  u3lem11 786  u3lem13b 790  bi1o1a 798  test 802  mlalem 832  bi3 839  bi4 840  orbi 842  mlaconj4 844  neg3antlem2 865  elimconslem 867  mhlemlem1 874  mhlem 876  marsdenlem3 882  marsdenlem4 883  mlaconjo 886  mhcor1 888  e2astlem1 895  govar 896  lem4.6.2e1 1079

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