Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  testmod1 GIF version

Theorem testmod1 1214
 Description: A modular law experiment. (Contributed by NM, 21-Apr-2012.)
Assertion
Ref Expression
testmod1 (((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))

Proof of Theorem testmod1
StepHypRef Expression
1 testmod 1213 . 2 (((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = ((b ∩ ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd)))) ∪ a)
2 orcom 73 . . 3 ((b ∩ ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd)))) ∪ a) = (a ∪ (b ∩ ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd)))))
3 orcom 73 . . . . . 6 ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd))) = (((ac) ∩ (bd)) ∪ (((ac) ∪ ((bc) ∩ (da))) ∩ d))
4 ancom 74 . . . . . . 7 (((ac) ∪ ((bc) ∩ (da))) ∩ d) = (d ∩ ((ac) ∪ ((bc) ∩ (da))))
54lor 70 . . . . . 6 (((ac) ∩ (bd)) ∪ (((ac) ∪ ((bc) ∩ (da))) ∩ d)) = (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))
63, 5tr 62 . . . . 5 ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd))) = (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))
76lan 77 . . . 4 (b ∩ ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd)))) = (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da))))))
87lor 70 . . 3 (a ∪ (b ∩ ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd))))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))
92, 8tr 62 . 2 ((b ∩ ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd)))) ∪ a) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))
101, 9tr 62 1 (((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))
 Colors of variables: term 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)
 Copyright terms: Public domain W3C validator