Theorem an32 83

Description: Swap conjuncts.

Assertion

Ref	Expression
an32	((a ^ b) ^ c) = ((a ^ c) ^ b)

Proof of Theorem an32

Step	Hyp	Ref	Expression
1		ancom 74	. . 3 (b ^ c) = (c ^ b)
2	1	lan 77	. 2 (a ^ (b ^ c)) = (a ^ (c ^ b))
3		anass 76	. 2 ((a ^ b) ^ c) = (a ^ (b ^ c))
4		anass 76	. 2 ((a ^ c) ^ b) = (a ^ (c ^ b))
5	2, 3, 4	3tr1 63	1 ((a ^ b) ^ c) = ((a ^ c) ^ b)

Syntax hints:   = wb 1   ^ wa 7

This theorem is referenced by:  lel 151  k1-4 359  wlel 392  gsth 489  i3bi 496  ud2lem2 564  ud3lem1a 566  ud3lem1b 567  ud3lem1d 569  ud3lem2 571  ud3lem3b 573  ud3lem3c 574  ud4lem1a 577  ud4lem1b 578  ud5lem1b 587  ud5lem2 590  ud5lem3a 591  ud5lem3b 592  ud5lem3c 593  u1lemaa 600  u3lemaa 602  u4lemaa 603  u5lemaa 604  u2lemana 606  u3lemana 607  u4lemana 608  u5lemana 609  u3lemab 612  u4lemab 613  u5lemab 614  u3lemanb 617  u2lem1 735  3vth7 810  3vded21 817  mlaoml 833  sadm3 838  bi3 839  bi4 840  mlaconj4 844  comanblem1 870  go2n4 899  gomaex3lem8 921  oa6v4v 933  oalem1 1005  oadistd 1023  4oadist 1043

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

This theorem depends on definitions:  df-a 40

Copyright terms: Public domain