QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  gomaex3h10 Unicode version
Theorem gomaex3h10 911
Description: Hypothesis for Godowski 6-var -> Mayet Example 3.
Hypotheses
Ref Expression
gomaex3h10.10 q = ((e v f) ->1 (b v c)')'
gomaex3h10.21 x = q
gomaex3h10.22 y = (e v f)'
Assertion
Ref Expression
gomaex3h10 x =< y'
Proof of Theorem gomaex3h10
StepHypRef Expression
1 lea 160 . . 3 ((e v f) ^ ((e v f) ^ (b v c)')') =< (e v f)
2 gomaex3h10.10 . . . 4 q = ((e v f) ->1 (b v c)')'
3 df-i1 44 . . . . . 6 ((e v f) ->1 (b v c)') = ((e v f)' v ((e v f) ^ (b v c)'))
43ax-r4 37 . . . . 5 ((e v f) ->1 (b v c)')' = ((e v f)' v ((e v f) ^ (b v c)'))'
5 anor1 88 . . . . . 6 ((e v f) ^ ((e v f) ^ (b v c)')') = ((e v f)' v ((e v f) ^ (b v c)'))'
65ax-r1 35 . . . . 5 ((e v f)' v ((e v f) ^ (b v c)'))' = ((e v f) ^ ((e v f) ^ (b v c)')')
74, 6ax-r2 36 . . . 4 ((e v f) ->1 (b v c)')' = ((e v f) ^ ((e v f) ^ (b v c)')')
82, 7ax-r2 36 . . 3 q = ((e v f) ^ ((e v f) ^ (b v c)')')
9 ax-a1 30 . . . 4 (e v f) = (e v f)''
109ax-r1 35 . . 3 (e v f)'' = (e v f)
111, 8, 10le3tr1 140 . 2 q =< (e v f)''
12 gomaex3h10.21 . 2 x = q
13 gomaex3h10.22 . . 3 y = (e v f)'
1413ax-r4 37 . 2 y' = (e v f)''
1511, 12, 14le3tr1 140 1 x =< y'
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-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-i1 44  df-le1 130  df-le2 131
This theorem is referenced by:  gomaex3lem5  918
  Copyright terms: Public domain W3C validator