QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3to4 Unicode version
Theorem oa3to4 951
Description: Orthoarguesian law (Godowski/Greechie 3-variable to 4-variable). The first 2 hypotheses are those for 4-OA. The next 3 are variable substitutions into 3-OA. The last is the 3-OA. The proof uses OM logic only.
Hypotheses
Ref Expression
oa3to4.oa4.1 a =< b'
oa3to4.oa4.2 c =< d'
oa3to4.3 g = ((b' ^ a') v (d' ^ c'))
oa3to4.4 e = b'
oa3to4.5 f = d'
oa3to4.oa3 (e ^ ((e ->1 g) v ((f ->1 g) ^ ((e ^ f) v ((e ->1 g) ^ (f ->1 g)))))) =< ((e ^ g) v (f ^ g))
Assertion
Ref Expression
oa3to4 ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
Proof of Theorem oa3to4
StepHypRef Expression
1 oa3to4.oa4.1 . . . 4 a =< b'
21lecon3 157 . . 3 b =< a'
3 oa3to4.oa4.2 . . . 4 c =< d'
43lecon3 157 . . 3 d =< c'
5 oa3to4.3 . . 3 g = ((b' ^ a') v (d' ^ c'))
6 oa3to4.4 . . 3 e = b'
7 oa3to4.5 . . 3 f = d'
8 oa3to4.oa3 . . 3 (e ^ ((e ->1 g) v ((f ->1 g) ^ ((e ^ f) v ((e ->1 g) ^ (f ->1 g)))))) =< ((e ^ g) v (f ^ g))
92, 4, 5, 6, 7, 8oa3to4lem6 950 . 2 ((b v a) ^ (d v c)) =< (b v (a ^ (c v ((b v d) ^ (a v c)))))
109oa3to4lem5 949 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  'wn 4   v wo 6   ^ wa 7   ->1 wi1 12
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-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator