Theorem an4 86

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 81	. . 3 (b ^ (c ^ d)) = (c ^ (b ^ d))
2	1	lan 77	. 2 (a ^ (b ^ (c ^ d))) = (a ^ (c ^ (b ^ d)))
3		anass 76	. 2 ((a ^ b) ^ (c ^ d)) = (a ^ (b ^ (c ^ d)))
4		anass 76	. 2 ((a ^ c) ^ (b ^ d)) = (a ^ (c ^ (b ^ d)))
5	2, 3, 4	3tr1 63	1 ((a ^ b) ^ (c ^ d)) = ((a ^ c) ^ (b ^ d))

Syntax hints:   = wb 1   ^ wa 7

This theorem is referenced by:  anandi 114  anandir 115  wwfh2 217  wfh2 424  fh2 470  gsth 489  i3bi 496  ud4lem1a 577  ud5lem1c 588  ud5lem3a 591  ud5lem3c 593  u5lembi 725  u3lem13b 790  3vth7 810  mlalem 832  bi3 839  bi4 840  mlaconj4 844  comanblem1 870  comanblem2 871  mhlem 876  mh 879  marsdenlem3 882  marsdenlem4 883  mhcor1 888  gomaex4 900  gomaex3lem8 921  vneulem16 1144  vneulemexp 1146

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