QLE Home Quantum Logic Explorer < Previous   Wrap >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  testmod3 Unicode version
Theorem testmod3 1215
Description: A modular law experiment.
Assertion
Ref Expression
testmod3 (((c v a) v ((b v c) ^ (d v a))) ^ (a v (b ^ (d v ((a v c) ^ (b v d)))))) = (a v (((c v a) v ((b v c) ^ (d v a))) ^ (b ^ (d v ((a v c) ^ (b v d))))))
Proof of Theorem testmod3
StepHypRef Expression
1 orcom 73 . . . 4 (a v (((c v a) v ((b v c) ^ (d v a))) ^ (b ^ (d v ((a v c) ^ (b v d)))))) = ((((c v a) v ((b v c) ^ (d v a))) ^ (b ^ (d v ((a v c) ^ (b v d))))) v a)
2 leor 159 . . . . . 6 a =< (c v a)
32ler 149 . . . . 5 a =< ((c v a) v ((b v c) ^ (d v a)))
43mli 1124 . . . 4 ((((c v a) v ((b v c) ^ (d v a))) ^ (b ^ (d v ((a v c) ^ (b v d))))) v a) = (((c v a) v ((b v c) ^ (d v a))) ^ ((b ^ (d v ((a v c) ^ (b v d)))) v a))
51, 4tr 62 . . 3 (a v (((c v a) v ((b v c) ^ (d v a))) ^ (b ^ (d v ((a v c) ^ (b v d)))))) = (((c v a) v ((b v c) ^ (d v a))) ^ ((b ^ (d v ((a v c) ^ (b v d)))) v a))
6 orcom 73 . . . 4 ((b ^ (d v ((a v c) ^ (b v d)))) v a) = (a v (b ^ (d v ((a v c) ^ (b v d)))))
76lan 77 . . 3 (((c v a) v ((b v c) ^ (d v a))) ^ ((b ^ (d v ((a v c) ^ (b v d)))) v a)) = (((c v a) v ((b v c) ^ (d v a))) ^ (a v (b ^ (d v ((a v c) ^ (b v d))))))
85, 7tr 62 . 2 (a v (((c v a) v ((b v c) ^ (d v a))) ^ (b ^ (d v ((a v c) ^ (b v d)))))) = (((c v a) v ((b v c) ^ (d v a))) ^ (a v (b ^ (d v ((a v c) ^ (b v d))))))
98cm 61 1 (((c v a) v ((b v c) ^ (d v a))) ^ (a v (b ^ (d v ((a v c) ^ (b v d)))))) = (a v (((c v a) v ((b v c) ^ (d v a))) ^ (b ^ (d v ((a v c) ^ (b v d))))))
Colors of variables: term
Syntax hints:   = wb 1   v 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 1120
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