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

Theorem 3vded21 817
Description: A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 31-Oct-1998.)
Hypotheses
Ref Expression
3vded21.1 c ≤ ((a0 b) →0 (c2 b))
3vded21.2 c ≤ (a0 b)
Assertion
Ref Expression
3vded21 cb

Proof of Theorem 3vded21
StepHypRef Expression
1 3vded21.2 . . . . . . 7 c ≤ (a0 b)
2 df-i0 43 . . . . . . 7 (a0 b) = (ab)
31, 2lbtr 139 . . . . . 6 c ≤ (ab)
4 3vded21.1 . . . . . . 7 c ≤ ((a0 b) →0 (c2 b))
5 df-i0 43 . . . . . . . 8 ((a0 b) →0 (c2 b)) = ((a0 b) ∪ (c2 b))
62ax-r4 37 . . . . . . . . 9 (a0 b) = (ab)
7 df-i2 45 . . . . . . . . . 10 (c2 b) = (b ∪ (cb ))
8 anor3 90 . . . . . . . . . . 11 (cb ) = (cb)
98lor 70 . . . . . . . . . 10 (b ∪ (cb )) = (b ∪ (cb) )
107, 9ax-r2 36 . . . . . . . . 9 (c2 b) = (b ∪ (cb) )
116, 102or 72 . . . . . . . 8 ((a0 b) ∪ (c2 b)) = ((ab) ∪ (b ∪ (cb) ))
12 ax-a2 31 . . . . . . . 8 ((ab) ∪ (b ∪ (cb) )) = ((b ∪ (cb) ) ∪ (ab) )
135, 11, 123tr 65 . . . . . . 7 ((a0 b) →0 (c2 b)) = ((b ∪ (cb) ) ∪ (ab) )
144, 13lbtr 139 . . . . . 6 c ≤ ((b ∪ (cb) ) ∪ (ab) )
153, 14ler2an 173 . . . . 5 c ≤ ((ab) ∩ ((b ∪ (cb) ) ∪ (ab) ))
16 comor2 462 . . . . . . . 8 (ab) C b
173leror 152 . . . . . . . . . . . 12 (cb) ≤ ((ab) ∪ b)
18 ax-a3 32 . . . . . . . . . . . . 13 ((ab) ∪ b) = (a ∪ (bb))
19 oridm 110 . . . . . . . . . . . . . 14 (bb) = b
2019lor 70 . . . . . . . . . . . . 13 (a ∪ (bb)) = (ab)
2118, 20ax-r2 36 . . . . . . . . . . . 12 ((ab) ∪ b) = (ab)
2217, 21lbtr 139 . . . . . . . . . . 11 (cb) ≤ (ab)
2322lecom 180 . . . . . . . . . 10 (cb) C (ab)
2423comcom 453 . . . . . . . . 9 (ab) C (cb)
2524comcom2 183 . . . . . . . 8 (ab) C (cb)
2616, 25com2or 483 . . . . . . 7 (ab) C (b ∪ (cb) )
27 comid 187 . . . . . . . 8 (ab) C (ab)
2827comcom2 183 . . . . . . 7 (ab) C (ab)
2926, 28fh1 469 . . . . . 6 ((ab) ∩ ((b ∪ (cb) ) ∪ (ab) )) = (((ab) ∩ (b ∪ (cb) )) ∪ ((ab) ∩ (ab) ))
30 or0 102 . . . . . . 7 ((((ab) ∩ b) ∪ ((ab) ∩ (cb) )) ∪ 0) = (((ab) ∩ b) ∪ ((ab) ∩ (cb) ))
3116, 25fh1 469 . . . . . . . . 9 ((ab) ∩ (b ∪ (cb) )) = (((ab) ∩ b) ∪ ((ab) ∩ (cb) ))
3231ax-r1 35 . . . . . . . 8 (((ab) ∩ b) ∪ ((ab) ∩ (cb) )) = ((ab) ∩ (b ∪ (cb) ))
33 dff 101 . . . . . . . 8 0 = ((ab) ∩ (ab) )
3432, 332or 72 . . . . . . 7 ((((ab) ∩ b) ∪ ((ab) ∩ (cb) )) ∪ 0) = (((ab) ∩ (b ∪ (cb) )) ∪ ((ab) ∩ (ab) ))
35 ax-a2 31 . . . . . . . . . 10 (ab) = (ba )
3635ran 78 . . . . . . . . 9 ((ab) ∩ b) = ((ba ) ∩ b)
37 ancom 74 . . . . . . . . 9 ((ba ) ∩ b) = (b ∩ (ba ))
38 anabs 121 . . . . . . . . 9 (b ∩ (ba )) = b
3936, 37, 383tr 65 . . . . . . . 8 ((ab) ∩ b) = b
4039ax-r5 38 . . . . . . 7 (((ab) ∩ b) ∪ ((ab) ∩ (cb) )) = (b ∪ ((ab) ∩ (cb) ))
4130, 34, 403tr2 64 . . . . . 6 (((ab) ∩ (b ∪ (cb) )) ∪ ((ab) ∩ (ab) )) = (b ∪ ((ab) ∩ (cb) ))
4229, 41ax-r2 36 . . . . 5 ((ab) ∩ ((b ∪ (cb) ) ∪ (ab) )) = (b ∪ ((ab) ∩ (cb) ))
4315, 42lbtr 139 . . . 4 c ≤ (b ∪ ((ab) ∩ (cb) ))
4443leran 153 . . 3 (c ∩ (cb)) ≤ ((b ∪ ((ab) ∩ (cb) )) ∩ (cb))
45 anabs 121 . . 3 (c ∩ (cb)) = c
46 comor2 462 . . . . 5 (cb) C b
47 comid 187 . . . . . . 7 (cb) C (cb)
4847comcom2 183 . . . . . 6 (cb) C (cb)
4923, 48com2an 484 . . . . 5 (cb) C ((ab) ∩ (cb) )
5046, 49fh1r 473 . . . 4 ((b ∪ ((ab) ∩ (cb) )) ∩ (cb)) = ((b ∩ (cb)) ∪ (((ab) ∩ (cb) ) ∩ (cb)))
51 ax-a2 31 . . . . . . 7 (cb) = (bc)
5251lan 77 . . . . . 6 (b ∩ (cb)) = (b ∩ (bc))
53 anabs 121 . . . . . 6 (b ∩ (bc)) = b
5452, 53ax-r2 36 . . . . 5 (b ∩ (cb)) = b
55 an32 83 . . . . . 6 (((ab) ∩ (cb) ) ∩ (cb)) = (((ab) ∩ (cb)) ∩ (cb) )
56 anass 76 . . . . . 6 (((ab) ∩ (cb)) ∩ (cb) ) = ((ab) ∩ ((cb) ∩ (cb) ))
57 dff 101 . . . . . . . . 9 0 = ((cb) ∩ (cb) )
5857lan 77 . . . . . . . 8 ((ab) ∩ 0) = ((ab) ∩ ((cb) ∩ (cb) ))
5958ax-r1 35 . . . . . . 7 ((ab) ∩ ((cb) ∩ (cb) )) = ((ab) ∩ 0)
60 an0 108 . . . . . . 7 ((ab) ∩ 0) = 0
6159, 60ax-r2 36 . . . . . 6 ((ab) ∩ ((cb) ∩ (cb) )) = 0
6255, 56, 613tr 65 . . . . 5 (((ab) ∩ (cb) ) ∩ (cb)) = 0
6354, 622or 72 . . . 4 ((b ∩ (cb)) ∪ (((ab) ∩ (cb) ) ∩ (cb))) = (b ∪ 0)
6450, 63ax-r2 36 . . 3 ((b ∪ ((ab) ∩ (cb) )) ∩ (cb)) = (b ∪ 0)
6544, 45, 64le3tr2 141 . 2 c ≤ (b ∪ 0)
66 or0 102 . 2 (b ∪ 0) = b
6765, 66lbtr 139 1 cb
Colors of variables: term
Syntax hints:  wle 2   wn 4  wo 6  wa 7  0wf 9  0 wi0 11  2 wi2 13
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-i0 43  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  3vded22  818
  Copyright terms: Public domain W3C validator