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

Theorem bi4 840
Description: Chained biconditional. (Contributed by NM, 25-Jun-2003.)
Assertion
Ref Expression
bi4 (((ab) ∩ (bc)) ∩ (cd)) = ((((ab) ∩ c) ∩ d) ∪ (((ab ) ∩ c ) ∩ d ))

Proof of Theorem bi4
StepHypRef Expression
1 bi3 839 . . 3 ((ab) ∩ (bc)) = (((ab) ∩ c) ∪ ((ab ) ∩ c ))
2 u12lembi 726 . . . 4 ((c1 d) ∩ (d2 c)) = (cd)
32ax-r1 35 . . 3 (cd) = ((c1 d) ∩ (d2 c))
41, 32an 79 . 2 (((ab) ∩ (bc)) ∩ (cd)) = ((((ab) ∩ c) ∪ ((ab ) ∩ c )) ∩ ((c1 d) ∩ (d2 c)))
5 df-i1 44 . . . . . 6 (c1 d) = (c ∪ (cd))
65lan 77 . . . . 5 ((((ab) ∩ c) ∪ ((ab ) ∩ c )) ∩ (c1 d)) = ((((ab) ∩ c) ∪ ((ab ) ∩ c )) ∩ (c ∪ (cd)))
7 leao2 163 . . . . . . 7 ((ab ) ∩ c ) ≤ (c ∪ (cd))
87lecom 180 . . . . . 6 ((ab ) ∩ c ) C (c ∪ (cd))
9 leao4 165 . . . . . . . . . 10 ((ab) ∩ c) ≤ ((ab )c)
10 oran2 92 . . . . . . . . . 10 ((ab )c) = ((ab ) ∩ c )
119, 10lbtr 139 . . . . . . . . 9 ((ab) ∩ c) ≤ ((ab ) ∩ c )
1211lecom 180 . . . . . . . 8 ((ab) ∩ c) C ((ab ) ∩ c )
1312comcom 453 . . . . . . 7 ((ab ) ∩ c ) C ((ab) ∩ c)
1413comcom6 459 . . . . . 6 ((ab ) ∩ c ) C ((ab) ∩ c)
158, 14fh2rc 480 . . . . 5 ((((ab) ∩ c) ∪ ((ab ) ∩ c )) ∩ (c ∪ (cd))) = ((((ab) ∩ c) ∩ (c ∪ (cd))) ∪ (((ab ) ∩ c ) ∩ (c ∪ (cd))))
16 comanr2 465 . . . . . . . . 9 c C ((ab) ∩ c)
1716comcom3 454 . . . . . . . 8 c C ((ab) ∩ c)
18 comanr1 464 . . . . . . . . 9 c C (cd)
1918comcom3 454 . . . . . . . 8 c C (cd)
2017, 19fh2 470 . . . . . . 7 (((ab) ∩ c) ∩ (c ∪ (cd))) = ((((ab) ∩ c) ∩ c ) ∪ (((ab) ∩ c) ∩ (cd)))
21 anass 76 . . . . . . . . 9 (((ab) ∩ c) ∩ c ) = ((ab) ∩ (cc ))
22 dff 101 . . . . . . . . . . 11 0 = (cc )
2322lan 77 . . . . . . . . . 10 ((ab) ∩ 0) = ((ab) ∩ (cc ))
2423ax-r1 35 . . . . . . . . 9 ((ab) ∩ (cc )) = ((ab) ∩ 0)
25 an0 108 . . . . . . . . 9 ((ab) ∩ 0) = 0
2621, 24, 253tr 65 . . . . . . . 8 (((ab) ∩ c) ∩ c ) = 0
27 anass 76 . . . . . . . . . 10 ((((ab) ∩ c) ∩ c) ∩ d) = (((ab) ∩ c) ∩ (cd))
2827ax-r1 35 . . . . . . . . 9 (((ab) ∩ c) ∩ (cd)) = ((((ab) ∩ c) ∩ c) ∩ d)
29 anass 76 . . . . . . . . . . 11 (((ab) ∩ c) ∩ c) = ((ab) ∩ (cc))
30 anidm 111 . . . . . . . . . . . 12 (cc) = c
3130lan 77 . . . . . . . . . . 11 ((ab) ∩ (cc)) = ((ab) ∩ c)
3229, 31ax-r2 36 . . . . . . . . . 10 (((ab) ∩ c) ∩ c) = ((ab) ∩ c)
3332ran 78 . . . . . . . . 9 ((((ab) ∩ c) ∩ c) ∩ d) = (((ab) ∩ c) ∩ d)
3428, 33ax-r2 36 . . . . . . . 8 (((ab) ∩ c) ∩ (cd)) = (((ab) ∩ c) ∩ d)
3526, 342or 72 . . . . . . 7 ((((ab) ∩ c) ∩ c ) ∪ (((ab) ∩ c) ∩ (cd))) = (0 ∪ (((ab) ∩ c) ∩ d))
36 or0r 103 . . . . . . 7 (0 ∪ (((ab) ∩ c) ∩ d)) = (((ab) ∩ c) ∩ d)
3720, 35, 363tr 65 . . . . . 6 (((ab) ∩ c) ∩ (c ∪ (cd))) = (((ab) ∩ c) ∩ d)
38 comanr2 465 . . . . . . . 8 c C ((ab ) ∩ c )
3938, 19fh2 470 . . . . . . 7 (((ab ) ∩ c ) ∩ (c ∪ (cd))) = ((((ab ) ∩ c ) ∩ c ) ∪ (((ab ) ∩ c ) ∩ (cd)))
40 anass 76 . . . . . . . . 9 (((ab ) ∩ c ) ∩ c ) = ((ab ) ∩ (cc ))
41 anidm 111 . . . . . . . . . 10 (cc ) = c
4241lan 77 . . . . . . . . 9 ((ab ) ∩ (cc )) = ((ab ) ∩ c )
4340, 42ax-r2 36 . . . . . . . 8 (((ab ) ∩ c ) ∩ c ) = ((ab ) ∩ c )
44 an4 86 . . . . . . . . 9 (((ab ) ∩ c ) ∩ (cd)) = (((ab ) ∩ c) ∩ (cd))
45 anass 76 . . . . . . . . 9 (((ab ) ∩ c) ∩ (cd)) = ((ab ) ∩ (c ∩ (cd)))
4622ran 78 . . . . . . . . . . . . 13 (0 ∩ d) = ((cc ) ∩ d)
4746ax-r1 35 . . . . . . . . . . . 12 ((cc ) ∩ d) = (0 ∩ d)
48 anass 76 . . . . . . . . . . . 12 ((cc ) ∩ d) = (c ∩ (cd))
49 an0r 109 . . . . . . . . . . . 12 (0 ∩ d) = 0
5047, 48, 493tr2 64 . . . . . . . . . . 11 (c ∩ (cd)) = 0
5150lan 77 . . . . . . . . . 10 ((ab ) ∩ (c ∩ (cd))) = ((ab ) ∩ 0)
52 an0 108 . . . . . . . . . 10 ((ab ) ∩ 0) = 0
5351, 52ax-r2 36 . . . . . . . . 9 ((ab ) ∩ (c ∩ (cd))) = 0
5444, 45, 533tr 65 . . . . . . . 8 (((ab ) ∩ c ) ∩ (cd)) = 0
5543, 542or 72 . . . . . . 7 ((((ab ) ∩ c ) ∩ c ) ∪ (((ab ) ∩ c ) ∩ (cd))) = (((ab ) ∩ c ) ∪ 0)
56 or0 102 . . . . . . 7 (((ab ) ∩ c ) ∪ 0) = ((ab ) ∩ c )
5739, 55, 563tr 65 . . . . . 6 (((ab ) ∩ c ) ∩ (c ∪ (cd))) = ((ab ) ∩ c )
5837, 572or 72 . . . . 5 ((((ab) ∩ c) ∩ (c ∪ (cd))) ∪ (((ab ) ∩ c ) ∩ (c ∪ (cd)))) = ((((ab) ∩ c) ∩ d) ∪ ((ab ) ∩ c ))
596, 15, 583tr 65 . . . 4 ((((ab) ∩ c) ∪ ((ab ) ∩ c )) ∩ (c1 d)) = ((((ab) ∩ c) ∩ d) ∪ ((ab ) ∩ c ))
6059ran 78 . . 3 (((((ab) ∩ c) ∪ ((ab ) ∩ c )) ∩ (c1 d)) ∩ (d2 c)) = (((((ab) ∩ c) ∩ d) ∪ ((ab ) ∩ c )) ∩ (d2 c))
61 anass 76 . . 3 (((((ab) ∩ c) ∪ ((ab ) ∩ c )) ∩ (c1 d)) ∩ (d2 c)) = ((((ab) ∩ c) ∪ ((ab ) ∩ c )) ∩ ((c1 d) ∩ (d2 c)))
62 anass 76 . . . . . . . 8 ((((ab) ∩ c) ∩ d) ∩ (d2 c)) = (((ab) ∩ c) ∩ (d ∩ (d2 c)))
63 an4 86 . . . . . . . 8 (((ab) ∩ c) ∩ (d ∩ (d2 c))) = (((ab) ∩ d) ∩ (c ∩ (d2 c)))
64 ancom 74 . . . . . . . . . . 11 (c ∩ (d2 c)) = ((d2 c) ∩ c)
65 u2lemab 611 . . . . . . . . . . 11 ((d2 c) ∩ c) = c
6664, 65ax-r2 36 . . . . . . . . . 10 (c ∩ (d2 c)) = c
6766lan 77 . . . . . . . . 9 (((ab) ∩ d) ∩ (c ∩ (d2 c))) = (((ab) ∩ d) ∩ c)
68 an32 83 . . . . . . . . 9 (((ab) ∩ d) ∩ c) = (((ab) ∩ c) ∩ d)
6967, 68ax-r2 36 . . . . . . . 8 (((ab) ∩ d) ∩ (c ∩ (d2 c))) = (((ab) ∩ c) ∩ d)
7062, 63, 693tr 65 . . . . . . 7 ((((ab) ∩ c) ∩ d) ∩ (d2 c)) = (((ab) ∩ c) ∩ d)
7170df2le1 135 . . . . . 6 (((ab) ∩ c) ∩ d) ≤ (d2 c)
7271lecom 180 . . . . 5 (((ab) ∩ c) ∩ d) C (d2 c)
73 an32 83 . . . . . . . . 9 (((ab) ∩ c) ∩ d) = (((ab) ∩ d) ∩ c)
74 leao4 165 . . . . . . . . 9 (((ab) ∩ d) ∩ c) ≤ ((ab )c)
7573, 74bltr 138 . . . . . . . 8 (((ab) ∩ c) ∩ d) ≤ ((ab )c)
7675, 10lbtr 139 . . . . . . 7 (((ab) ∩ c) ∩ d) ≤ ((ab ) ∩ c )
7776lecom 180 . . . . . 6 (((ab) ∩ c) ∩ d) C ((ab ) ∩ c )
7877comcom7 460 . . . . 5 (((ab) ∩ c) ∩ d) C ((ab ) ∩ c )
7972, 78fh2r 474 . . . 4 (((((ab) ∩ c) ∩ d) ∪ ((ab ) ∩ c )) ∩ (d2 c)) = (((((ab) ∩ c) ∩ d) ∩ (d2 c)) ∪ (((ab ) ∩ c ) ∩ (d2 c)))
80 anass 76 . . . . . 6 (((ab ) ∩ c ) ∩ (d2 c)) = ((ab ) ∩ (c ∩ (d2 c)))
81 ancom 74 . . . . . . . 8 (c ∩ (d2 c)) = ((d2 c) ∩ c )
82 u2lemanb 616 . . . . . . . 8 ((d2 c) ∩ c ) = (dc )
8381, 82ax-r2 36 . . . . . . 7 (c ∩ (d2 c)) = (dc )
8483lan 77 . . . . . 6 ((ab ) ∩ (c ∩ (d2 c))) = ((ab ) ∩ (dc ))
85 an12 81 . . . . . . 7 ((ab ) ∩ (dc )) = (d ∩ ((ab ) ∩ c ))
86 ancom 74 . . . . . . 7 (d ∩ ((ab ) ∩ c )) = (((ab ) ∩ c ) ∩ d )
8785, 86ax-r2 36 . . . . . 6 ((ab ) ∩ (dc )) = (((ab ) ∩ c ) ∩ d )
8880, 84, 873tr 65 . . . . 5 (((ab ) ∩ c ) ∩ (d2 c)) = (((ab ) ∩ c ) ∩ d )
8970, 882or 72 . . . 4 (((((ab) ∩ c) ∩ d) ∩ (d2 c)) ∪ (((ab ) ∩ c ) ∩ (d2 c))) = ((((ab) ∩ c) ∩ d) ∪ (((ab ) ∩ c ) ∩ d ))
9079, 89ax-r2 36 . . 3 (((((ab) ∩ c) ∩ d) ∪ ((ab ) ∩ c )) ∩ (d2 c)) = ((((ab) ∩ c) ∩ d) ∪ (((ab ) ∩ c ) ∩ d ))
9160, 61, 903tr2 64 . 2 ((((ab) ∩ c) ∪ ((ab ) ∩ c )) ∩ ((c1 d) ∩ (d2 c))) = ((((ab) ∩ c) ∩ d) ∪ (((ab ) ∩ c ) ∩ d ))
924, 91ax-r2 36 1 (((ab) ∩ (bc)) ∩ (cd)) = ((((ab) ∩ c) ∩ d) ∪ (((ab ) ∩ c ) ∩ d ))
Colors of variables: term
Syntax hints:   = wb 1   wn 4  tb 5  wo 6  wa 7  0wf 9  1 wi1 12  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-i1 44  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  mhcor1  888
  Copyright terms: Public domain W3C validator