Theorem an4 78

Description: Swap conjuncts.

Assertion

Ref	Expression
an4	((a ^ b) ^ (c ^ d)) = ((a ^ c) ^ (b ^ d))

Proof of Theorem an4

Step	Hyp	Ref	Expression
1		an12 74	. . 3 (b ^ (c ^ d)) = (c ^ (b ^ d))
2	1	lan 70	. 2 (a ^ (b ^ (c ^ d))) = (a ^ (c ^ (b ^ d)))
3		anass 69	. 2 ((a ^ b) ^ (c ^ d)) = (a ^ (b ^ (c ^ d)))
4		anass 69	. 2 ((a ^ c) ^ (b ^ d)) = (a ^ (c ^ (b ^ d)))
5	2, 3, 4	3tr1 60	1 ((a ^ b) ^ (c ^ d)) = ((a ^ c) ^ (b ^ d))

Syntax hints:   = wb 1   ^ wa 7

This theorem is referenced by:  anandi 106  anandir 107  wwfh2 209  wfh2 406  fh2 452  gsth 471  i3bi 478  ud4lem1a 559  ud5lem1c 570  ud5lem3a 573  ud5lem3c 575  u5lembi 707  u3lem13b 772  3vth7 792  mlalem 814  bi3 821  bi4 822  mlaconj4 826  comanblem1 852  comanblem2 853  mhlem 858  mh 861  marsdenlem3 864  marsdenlem4 865  mhcor1 870  gomaex4 880  gomaex3lem8 901

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

This theorem depends on definitions:  df-a 39

metamath.org