QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa6v4v Unicode version
Theorem oa6v4v 933
Description: 6-variable OA to 4-variable OA.
Hypotheses
Ref Expression
oa6v4v.1 (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
oa6v4v.2 e = 0
oa6v4v.3 f = 1
Assertion
Ref Expression
oa6v4v ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
Proof of Theorem oa6v4v
StepHypRef Expression
1 oa6v4v.1 . 2 (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
2 oa6v4v.2 . . . . . 6 e = 0
3 oa6v4v.3 . . . . . 6 f = 1
42, 32or 72 . . . . 5 (e v f) = (0 v 1)
5 or0r 103 . . . . 5 (0 v 1) = 1
64, 5ax-r2 36 . . . 4 (e v f) = 1
76lan 77 . . 3 (((a v b) ^ (c v d)) ^ (e v f)) = (((a v b) ^ (c v d)) ^ 1)
8 an1 106 . . 3 (((a v b) ^ (c v d)) ^ 1) = ((a v b) ^ (c v d))
97, 8ax-r2 36 . 2 (((a v b) ^ (c v d)) ^ (e v f)) = ((a v b) ^ (c v d))
102lor 70 . . . . . . . . . . 11 (a v e) = (a v 0)
11 or0 102 . . . . . . . . . . 11 (a v 0) = a
1210, 11ax-r2 36 . . . . . . . . . 10 (a v e) = a
133lor 70 . . . . . . . . . . 11 (b v f) = (b v 1)
14 or1 104 . . . . . . . . . . 11 (b v 1) = 1
1513, 14ax-r2 36 . . . . . . . . . 10 (b v f) = 1
1612, 152an 79 . . . . . . . . 9 ((a v e) ^ (b v f)) = (a ^ 1)
17 an1 106 . . . . . . . . 9 (a ^ 1) = a
1816, 17ax-r2 36 . . . . . . . 8 ((a v e) ^ (b v f)) = a
192lor 70 . . . . . . . . . . 11 (c v e) = (c v 0)
20 or0 102 . . . . . . . . . . 11 (c v 0) = c
2119, 20ax-r2 36 . . . . . . . . . 10 (c v e) = c
223lor 70 . . . . . . . . . . 11 (d v f) = (d v 1)
23 or1 104 . . . . . . . . . . 11 (d v 1) = 1
2422, 23ax-r2 36 . . . . . . . . . 10 (d v f) = 1
2521, 242an 79 . . . . . . . . 9 ((c v e) ^ (d v f)) = (c ^ 1)
26 an1 106 . . . . . . . . 9 (c ^ 1) = c
2725, 26ax-r2 36 . . . . . . . 8 ((c v e) ^ (d v f)) = c
2818, 272or 72 . . . . . . 7 (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))) = (a v c)
2928lan 77 . . . . . 6 (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))) = (((a v c) ^ (b v d)) ^ (a v c))
30 an32 83 . . . . . . 7 (((a v c) ^ (b v d)) ^ (a v c)) = (((a v c) ^ (a v c)) ^ (b v d))
31 anidm 111 . . . . . . . 8 ((a v c) ^ (a v c)) = (a v c)
3231ran 78 . . . . . . 7 (((a v c) ^ (a v c)) ^ (b v d)) = ((a v c) ^ (b v d))
3330, 32ax-r2 36 . . . . . 6 (((a v c) ^ (b v d)) ^ (a v c)) = ((a v c) ^ (b v d))
3429, 33ax-r2 36 . . . . 5 (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))) = ((a v c) ^ (b v d))
3534lor 70 . . . 4 (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))))) = (c v ((a v c) ^ (b v d)))
3635lan 77 . . 3 (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))) = (a ^ (c v ((a v c) ^ (b v d))))
3736lor 70 . 2 (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))))))) = (b v (a ^ (c v ((a v c) ^ (b v d)))))
381, 9, 37le3tr2 141 1 ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2   v wo 6   ^ wa 7  1wt 8  0wf 9
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
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:  oa64v  1031
  Copyright terms: Public domain W3C validator