QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  gomaex3lem1 Unicode version
Theorem gomaex3lem1 914
Description: Lemma for Godowski 6-var -> Mayet Example 3.
Hypothesis
Ref Expression
gomaex3lem1.3 c =< d'
Assertion
Ref Expression
gomaex3lem1 (c v (c v d)') = d'
Proof of Theorem gomaex3lem1
StepHypRef Expression
1 comid 187 . . . 4 c C c
21comcom2 183 . . 3 c C c'
3 gomaex3lem1.3 . . . 4 c =< d'
43lecom 180 . . 3 c C d'
52, 4fh3 471 . 2 (c v (c' ^ d')) = ((c v c') ^ (c v d'))
6 anor3 90 . . 3 (c' ^ d') = (c v d)'
76lor 70 . 2 (c v (c' ^ d')) = (c v (c v d)')
8 ancom 74 . . 3 ((c v c') ^ (c v d')) = ((c v d') ^ (c v c'))
93df-le2 131 . . . . . 6 (c v d') = d'
109ax-r1 35 . . . . 5 d' = (c v d')
11 df-t 41 . . . . 5 1 = (c v c')
1210, 112an 79 . . . 4 (d' ^ 1) = ((c v d') ^ (c v c'))
1312ax-r1 35 . . 3 ((c v d') ^ (c v c')) = (d' ^ 1)
14 an1 106 . . 3 (d' ^ 1) = d'
158, 13, 143tr 65 . 2 ((c v c') ^ (c v d')) = d'
165, 7, 153tr2 64 1 (c v (c v d)') = d'
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2  'wn 4   v wo 6   ^ wa 7  1wt 8
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-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  gomaex3lem7  920
  Copyright terms: Public domain W3C validator