QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wlem14 GIF version

Theorem wlem14 430
Description: Lemma for KA14 soundness. (Contributed by NM, 25-Oct-1997.)
Assertion
Ref Expression
wlem14 (((ab ) ∪ a ) ∪ ((ab ) ∪ ((a ∩ ((ab ) ∩ (ab))) ∪ (a ∩ ((ab ) ∩ (ab)) )))) = 1

Proof of Theorem wlem14
StepHypRef Expression
1 df-t 41 . . . 4 1 = (((ab ) ∪ a ) ∪ ((ab ) ∪ a ) )
21ax-r1 35 . . 3 (((ab ) ∪ a ) ∪ ((ab ) ∪ a ) ) = 1
3 ax-a2 31 . . . 4 (((ab ) ∪ a ) ∪ ((ab ) ∪ a )) = (((ab ) ∪ a ) ∪ ((ab ) ∪ a ) )
43bi1 118 . . 3 ((((ab ) ∪ a ) ∪ ((ab ) ∪ a )) ≡ (((ab ) ∪ a ) ∪ ((ab ) ∪ a ) )) = 1
52, 4wwbmpr 206 . 2 (((ab ) ∪ a ) ∪ ((ab ) ∪ a )) = 1
6 df-t 41 . . . . . . . 8 1 = (((ab ) ∩ (ab)) ∪ ((ab ) ∩ (ab)) )
76ax-r1 35 . . . . . . 7 (((ab ) ∩ (ab)) ∪ ((ab ) ∩ (ab)) ) = 1
87bi1 118 . . . . . 6 ((((ab ) ∩ (ab)) ∪ ((ab ) ∩ (ab)) ) ≡ 1) = 1
98wlan 370 . . . . 5 ((a ∩ (((ab ) ∩ (ab)) ∪ ((ab ) ∩ (ab)) )) ≡ (a ∩ 1)) = 1
10 anidm 111 . . . . . . . . . . 11 (aa) = a
1110bi1 118 . . . . . . . . . 10 ((aa) ≡ a) = 1
1211wr1 197 . . . . . . . . 9 (a ≡ (aa)) = 1
13 wleo 387 . . . . . . . . . 10 (a2 (ab )) = 1
14 wleo 387 . . . . . . . . . 10 (a2 (ab)) = 1
1513, 14wle2an 404 . . . . . . . . 9 ((aa) ≤2 ((ab ) ∩ (ab))) = 1
1612, 15wbltr 397 . . . . . . . 8 (a2 ((ab ) ∩ (ab))) = 1
1716wlecom 409 . . . . . . 7 C (a, ((ab ) ∩ (ab))) = 1
1817wcomcom3 416 . . . . . 6 C (a , ((ab ) ∩ (ab))) = 1
1917wcomcom4 417 . . . . . 6 C (a , ((ab ) ∩ (ab)) ) = 1
2018, 19wfh1 423 . . . . 5 ((a ∩ (((ab ) ∩ (ab)) ∪ ((ab ) ∩ (ab)) )) ≡ ((a ∩ ((ab ) ∩ (ab))) ∪ (a ∩ ((ab ) ∩ (ab)) ))) = 1
21 an1 106 . . . . . 6 (a ∩ 1) = a
2221bi1 118 . . . . 5 ((a ∩ 1) ≡ a ) = 1
239, 20, 22w3tr2 375 . . . 4 (((a ∩ ((ab ) ∩ (ab))) ∪ (a ∩ ((ab ) ∩ (ab)) )) ≡ a ) = 1
2423wlor 368 . . 3 (((ab ) ∪ ((a ∩ ((ab ) ∩ (ab))) ∪ (a ∩ ((ab ) ∩ (ab)) ))) ≡ ((ab ) ∪ a )) = 1
2524wlor 368 . 2 ((((ab ) ∪ a ) ∪ ((ab ) ∪ ((a ∩ ((ab ) ∩ (ab))) ∪ (a ∩ ((ab ) ∩ (ab)) )))) ≡ (((ab ) ∪ a ) ∪ ((ab ) ∪ a ))) = 1
265, 25wwbmpr 206 1 (((ab ) ∪ a ) ∪ ((ab ) ∪ ((a ∩ ((ab ) ∩ (ab))) ∪ (a ∩ ((ab ) ∩ (ab)) )))) = 1
Colors of variables: term
Syntax hints:   = wb 1   wn 4  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-wom 361
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator