QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa64v Unicode version
Theorem oa64v 1031
Description: Derivation of 4-variable OA from 6-variable OA.
Hypotheses
Ref Expression
oa64v.1 a =< b'
oa64v.2 c =< d'
Assertion
Ref Expression
oa64v ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
Proof of Theorem oa64v
StepHypRef Expression
1 oa64v.1 . . 3 a =< b'
2 oa64v.2 . . 3 c =< d'
3 le0 147 . . 3 0 =< 1'
41, 2, 3ax-oa6 1030 . 2 (((a v b) ^ (c v d)) ^ (0 v 1)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v 0) ^ (b v 1)) v ((c v 0) ^ (d v 1)))))))
5 id 59 . 2 0 = 0
6 id 59 . 2 1 = 1
74, 5, 6oa6v4v 933 1 ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   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  ax-oa6 1030
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:  oa63v  1032
  Copyright terms: Public domain W3C validator