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

Theorem cancellem 891
Description: Lemma for cancellation law eliminating 1 consequent. (Contributed by NM, 21-Feb-2002.)
Hypothesis
Ref Expression
cancel.1 ((d ∪ (a1 c)) →1 c) = ((d ∪ (b1 c)) →1 c)
Assertion
Ref Expression
cancellem (d ∪ (a1 c)) ≤ (d ∪ (b1 c))

Proof of Theorem cancellem
StepHypRef Expression
1 i1abs 801 . . 3 (((d ∪ (a1 c)) →1 c) ∪ ((d ∪ (a1 c)) ∩ c)) = (d ∪ (a1 c))
21ax-r1 35 . 2 (d ∪ (a1 c)) = (((d ∪ (a1 c)) →1 c) ∪ ((d ∪ (a1 c)) ∩ c))
3 leo 158 . . . . 5 (d ∪ (b1 c)) ≤ ((d ∪ (b1 c)) ∪ ((d ∪ (b1 c)) ∩ c))
4 cancel.1 . . . . . . 7 ((d ∪ (a1 c)) →1 c) = ((d ∪ (b1 c)) →1 c)
5 df-i1 44 . . . . . . 7 ((d ∪ (b1 c)) →1 c) = ((d ∪ (b1 c)) ∪ ((d ∪ (b1 c)) ∩ c))
64, 5ax-r2 36 . . . . . 6 ((d ∪ (a1 c)) →1 c) = ((d ∪ (b1 c)) ∪ ((d ∪ (b1 c)) ∩ c))
76ax-r1 35 . . . . 5 ((d ∪ (b1 c)) ∪ ((d ∪ (b1 c)) ∩ c)) = ((d ∪ (a1 c)) →1 c)
83, 7lbtr 139 . . . 4 (d ∪ (b1 c)) ≤ ((d ∪ (a1 c)) →1 c)
98lecon2 156 . . 3 ((d ∪ (a1 c)) →1 c) ≤ (d ∪ (b1 c))
10 leor 159 . . . . . 6 ((d ∪ (a1 c)) ∩ c) ≤ ((d ∪ (a1 c)) ∪ ((d ∪ (a1 c)) ∩ c))
11 df-i1 44 . . . . . . . 8 ((d ∪ (a1 c)) →1 c) = ((d ∪ (a1 c)) ∪ ((d ∪ (a1 c)) ∩ c))
1211ax-r1 35 . . . . . . 7 ((d ∪ (a1 c)) ∪ ((d ∪ (a1 c)) ∩ c)) = ((d ∪ (a1 c)) →1 c)
1312, 4ax-r2 36 . . . . . 6 ((d ∪ (a1 c)) ∪ ((d ∪ (a1 c)) ∩ c)) = ((d ∪ (b1 c)) →1 c)
1410, 13lbtr 139 . . . . 5 ((d ∪ (a1 c)) ∩ c) ≤ ((d ∪ (b1 c)) →1 c)
15 lear 161 . . . . 5 ((d ∪ (a1 c)) ∩ c) ≤ c
1614, 15ler2an 173 . . . 4 ((d ∪ (a1 c)) ∩ c) ≤ (((d ∪ (b1 c)) →1 c) ∩ c)
17 coman2 186 . . . . . . 7 ((d ∪ (b1 c)) ∩ c) C c
18 coman1 185 . . . . . . . 8 ((d ∪ (b1 c)) ∩ c) C (d ∪ (b1 c))
1918comcom2 183 . . . . . . 7 ((d ∪ (b1 c)) ∩ c) C (d ∪ (b1 c))
2017, 19fh2rc 480 . . . . . 6 (((d ∪ (b1 c)) ∪ ((d ∪ (b1 c)) ∩ c)) ∩ c) = (((d ∪ (b1 c))c) ∪ (((d ∪ (b1 c)) ∩ c) ∩ c))
215ran 78 . . . . . 6 (((d ∪ (b1 c)) →1 c) ∩ c) = (((d ∪ (b1 c)) ∪ ((d ∪ (b1 c)) ∩ c)) ∩ c)
22 id 59 . . . . . 6 (((d ∪ (b1 c))c) ∪ (((d ∪ (b1 c)) ∩ c) ∩ c)) = (((d ∪ (b1 c))c) ∪ (((d ∪ (b1 c)) ∩ c) ∩ c))
2320, 21, 223tr1 63 . . . . 5 (((d ∪ (b1 c)) →1 c) ∩ c) = (((d ∪ (b1 c))c) ∪ (((d ∪ (b1 c)) ∩ c) ∩ c))
24 leao4 165 . . . . . . . 8 ((d ∩ (bc) ) ∩ (bc)) ≤ (b ∪ (bc))
2524lerr 150 . . . . . . 7 ((d ∩ (bc) ) ∩ (bc)) ≤ (d ∪ (b ∪ (bc)))
26 df-i1 44 . . . . . . . . . . . 12 (b1 c) = (b ∪ (bc))
2726lor 70 . . . . . . . . . . 11 (d ∪ (b1 c)) = (d ∪ (b ∪ (bc)))
2827ax-r4 37 . . . . . . . . . 10 (d ∪ (b1 c)) = (d ∪ (b ∪ (bc)))
29 an12 81 . . . . . . . . . . . 12 (b ∩ (d ∩ (bc) )) = (d ∩ (b ∩ (bc) ))
30 anor1 88 . . . . . . . . . . . . 13 (b ∩ (bc) ) = (b ∪ (bc))
3130lan 77 . . . . . . . . . . . 12 (d ∩ (b ∩ (bc) )) = (d ∩ (b ∪ (bc)) )
32 anor3 90 . . . . . . . . . . . 12 (d ∩ (b ∪ (bc)) ) = (d ∪ (b ∪ (bc)))
3329, 31, 323tr 65 . . . . . . . . . . 11 (b ∩ (d ∩ (bc) )) = (d ∪ (b ∪ (bc)))
3433ax-r1 35 . . . . . . . . . 10 (d ∪ (b ∪ (bc))) = (b ∩ (d ∩ (bc) ))
35 ancom 74 . . . . . . . . . 10 (b ∩ (d ∩ (bc) )) = ((d ∩ (bc) ) ∩ b)
3628, 34, 353tr 65 . . . . . . . . 9 (d ∪ (b1 c)) = ((d ∩ (bc) ) ∩ b)
3736ran 78 . . . . . . . 8 ((d ∪ (b1 c))c) = (((d ∩ (bc) ) ∩ b) ∩ c)
38 anass 76 . . . . . . . 8 (((d ∩ (bc) ) ∩ b) ∩ c) = ((d ∩ (bc) ) ∩ (bc))
3937, 38ax-r2 36 . . . . . . 7 ((d ∪ (b1 c))c) = ((d ∩ (bc) ) ∩ (bc))
4025, 39, 27le3tr1 140 . . . . . 6 ((d ∪ (b1 c))c) ≤ (d ∪ (b1 c))
41 lea 160 . . . . . . 7 ((d ∪ (b1 c)) ∩ c) ≤ (d ∪ (b1 c))
4241lel 151 . . . . . 6 (((d ∪ (b1 c)) ∩ c) ∩ c) ≤ (d ∪ (b1 c))
4340, 42lel2or 170 . . . . 5 (((d ∪ (b1 c))c) ∪ (((d ∪ (b1 c)) ∩ c) ∩ c)) ≤ (d ∪ (b1 c))
4423, 43bltr 138 . . . 4 (((d ∪ (b1 c)) →1 c) ∩ c) ≤ (d ∪ (b1 c))
4516, 44letr 137 . . 3 ((d ∪ (a1 c)) ∩ c) ≤ (d ∪ (b1 c))
469, 45lel2or 170 . 2 (((d ∪ (a1 c)) →1 c) ∪ ((d ∪ (a1 c)) ∩ c)) ≤ (d ∪ (b1 c))
472, 46bltr 138 1 (d ∪ (a1 c)) ≤ (d ∪ (b1 c))
Colors of variables: term
Syntax hints:   = wb 1  wle 2   wn 4  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:  cancel  892
  Copyright terms: Public domain W3C validator