Theorem comcom2 183

Description: Commutation equivalence. Kalmbach 83 p. 23. Does not use OML.

Hypothesis

Ref	Expression
comcom2.1	a C b

Assertion

Ref	Expression
comcom2	a C b'

Proof of Theorem comcom2

Step	Hyp	Ref	Expression
1		comcom2.1	. . . . 5 a C b
2	1	df-c2 133	. . . 4 a = ((a ^ b) v (a ^ b'))
3		ax-a1 30	. . . . . 6 b = b''
4	3	lan 77	. . . . 5 (a ^ b) = (a ^ b'')
5	4	ax-r5 38	. . . 4 ((a ^ b) v (a ^ b')) = ((a ^ b'') v (a ^ b'))
6	2, 5	ax-r2 36	. . 3 a = ((a ^ b'') v (a ^ b'))
7		ax-a2 31	. . 3 ((a ^ b'') v (a ^ b')) = ((a ^ b') v (a ^ b''))
8	6, 7	ax-r2 36	. 2 a = ((a ^ b') v (a ^ b''))
9	8	df-c1 132	1 a C b'

Syntax hints:   C wc 3  'wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  wwfh2 217  wwfh3 218  wwfh4 219  comcom3 454  comcom4 455  comcom6 459  fh1 469  fh2 470  nbdi 486  oml4 487  gsth 489  gsth2 490  i3bi 496  df2i3 498  dfi3b 499  oi3ai3 503  i3lem2 505  comi31 508  com2i3 509  i3abs3 524  i3con 551  i3orlem7 558  i3orlem8 559  ud1lem1 560  ud1lem3 562  ud2lem3 565  ud3lem1a 566  ud3lem1b 567  ud3lem1c 568  ud3lem1d 569  ud3lem1 570  ud3lem2 571  ud3lem3d 575  ud3lem3 576  ud4lem1a 577  ud4lem1b 578  ud4lem1c 579  ud4lem1d 580  ud4lem1 581  ud4lem2 582  ud4lem3b 584  ud4lem3 585  ud5lem1a 586  ud5lem1b 587  ud5lem1 589  ud5lem3a 591  ud5lem3 594  u1lemaa 600  u4lemaa 603  u1lemab 610  u1lemanb 615  u3lemanb 617  u4lemoa 623  u4lemona 628  u3lemob 632  u4lemob 633  u3lemonb 637  u1lemc1 680  u4lemc1 683  u1lemc2 686  u2lemc2 687  u4lemc2 689  u5lemc2 690  u1lemc4 701  u3lemc4 703  u4lemc4 704  u5lemc4 705  u1lemle2 715  u1lembi 720  u5lembi 725  u4lem1 737  u1lem4 757  u4lem4 759  u4lem5 764  u5lem5 765  u4lem6 768  u5lem6 769  u1lem8 776  u1lem11 780  u3lem11 786  u3lem13a 789  u3lem13b 790  u3lem15 795  bi1o1a 798  test 802  test2 803  3vth5 808  3vded21 817  1oa 820  2oath1 826  neg3antlem2 865  elimcons 868  comanblem1 870  mhlem1 877  marsdenlem2 881  mlaconjolem 885  cancellem 891  e2ast2 894  govar 896  gomaex3lem1 914  gomaex3lem2 915  gomaex3lem3 916  oa23 936  lem4.6.2e1 1079  com3iia 1099

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-c1 132  df-c2 133

Copyright terms: Public domain