Theorem comcom2 175

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 125	. . . 4 a = ((a ^ b) v (a ^ b_|_))
3		ax-a1 29	. . . . . 6 b = b_|__|_
4	3	lan 70	. . . . 5 (a ^ b) = (a ^ b_|__|_)
5	4	ax-r5 37	. . . 4 ((a ^ b) v (a ^ b_|_)) = ((a ^ b_|__|_) v (a ^ b_|_))
6	2, 5	ax-r2 35	. . 3 a = ((a ^ b_|__|_) v (a ^ b_|_))
7		ax-a2 30	. . 3 ((a ^ b_|__|_) v (a ^ b_|_)) = ((a ^ b_|_) v (a ^ b_|__|_))
8	6, 7	ax-r2 35	. 2 a = ((a ^ b_|_) v (a ^ b_|__|_))
9	8	df-c1 124	1 a C b_|_

Syntax hints:   C wc 3  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  wwfh2 209  wwfh3 210  wwfh4 211  comcom3 436  comcom4 437  comcom6 441  fh1 451  fh2 452  nbdi 468  oml4 469  gsth 471  gsth2 472  i3bi 478  df2i3 480  dfi3b 481  oi3ai3 485  i3lem2 487  comi31 490  com2i3 491  i3abs3 506  i3con 533  i3orlem7 540  i3orlem8 541  ud1lem1 542  ud1lem3 544  ud2lem3 547  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1d 551  ud3lem1 552  ud3lem2 553  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud4lem2 564  ud4lem3b 566  ud4lem3 567  ud5lem1a 568  ud5lem1b 569  ud5lem1 571  ud5lem3a 573  ud5lem3 576  u1lemaa 582  u4lemaa 585  u1lemab 592  u1lemanb 597  u3lemanb 599  u4lemoa 605  u4lemona 610  u3lemob 614  u4lemob 615  u3lemonb 619  u1lemc1 662  u4lemc1 665  u1lemc2 668  u2lemc2 669  u4lemc2 671  u5lemc2 672  u1lemc4 683  u3lemc4 685  u4lemc4 686  u5lemc4 687  u1lemle2 697  u1lembi 702  u5lembi 707  u4lem1 719  u1lem4 739  u4lem4 741  u4lem5 746  u5lem5 747  u4lem6 750  u5lem6 751  u1lem8 758  u1lem11 762  u3lem11 768  u3lem13a 771  u3lem13b 772  u3lem15 777  bi1o1a 780  test 784  test2 785  3vth5 790  3vded21 799  1oa 802  2oath1 808  neg3antlem2 847  elimcons 850  comanblem1 852  mhlem1 859  marsdenlem2 863  mlaconjolem 867  cancellem 873  govar 876  gomaex3lem1 894  gomaex3lem2 895  gomaex3lem3 896  oa23 916

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

This theorem depends on definitions:  df-a 39  df-c1 124  df-c2 125

metamath.org