Theorem testmod1 1214

Description: A modular law experiment. (Contributed by NM, 21-Apr-2012.)

Assertion

Ref	Expression
testmod1	(((c ∪ a) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))) = (a ∪ (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))))

Proof of Theorem testmod1

Step	Hyp	Ref	Expression
1		testmod 1213	. 2 (((c ∪ a) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))) = ((b ∩ ((((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d) ∪ ((a ∪ c) ∩ (b ∪ d)))) ∪ a)
2		orcom 73	. . 3 ((b ∩ ((((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d) ∪ ((a ∪ c) ∩ (b ∪ d)))) ∪ a) = (a ∪ (b ∩ ((((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d) ∪ ((a ∪ c) ∩ (b ∪ d)))))
3		orcom 73	. . . . . 6 ((((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d) ∪ ((a ∪ c) ∩ (b ∪ d))) = (((a ∪ c) ∩ (b ∪ d)) ∪ (((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d))
4		ancom 74	. . . . . . 7 (((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d) = (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))))
5	4	lor 70	. . . . . 6 (((a ∪ c) ∩ (b ∪ d)) ∪ (((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d)) = (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))
6	3, 5	tr 62	. . . . 5 ((((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d) ∪ ((a ∪ c) ∩ (b ∪ d))) = (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))
7	6	lan 77	. . . 4 (b ∩ ((((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d) ∪ ((a ∪ c) ∩ (b ∪ d)))) = (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))))))
8	7	lor 70	. . 3 (a ∪ (b ∩ ((((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d) ∪ ((a ∪ c) ∩ (b ∪ d))))) = (a ∪ (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))))
9	2, 8	tr 62	. 2 ((b ∩ ((((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d) ∪ ((a ∪ c) ∩ (b ∪ d)))) ∪ a) = (a ∪ (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))))
10	1, 9	tr 62	1 (((c ∪ a) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))) = (a ∪ (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))))

Syntax hints:   = wb 1   ∪ wo 6   ∩ wa 7

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

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by: (None)