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

Theorem u5lembi 725
 Description: Relevance implication and biconditional.
Assertion
Ref Expression
u5lembi ((a5 b) ∩ (b5 a)) = (ab)

Proof of Theorem u5lembi
StepHypRef Expression
1 u5lemc1b 685 . . . . . . 7 b C (a5 b)
21comcom 453 . . . . . 6 (a5 b) C b
3 u5lemc1 684 . . . . . . 7 a C (a5 b)
43comcom 453 . . . . . 6 (a5 b) C a
52, 4com2an 484 . . . . 5 (a5 b) C (ba)
62comcom2 183 . . . . . 6 (a5 b) C b
76, 4com2an 484 . . . . 5 (a5 b) C (ba)
85, 7com2or 483 . . . 4 (a5 b) C ((ba) ∪ (ba))
94comcom2 183 . . . . 5 (a5 b) C a
106, 9com2an 484 . . . 4 (a5 b) C (ba )
118, 10fh1 469 . . 3 ((a5 b) ∩ (((ba) ∪ (ba)) ∪ (ba ))) = (((a5 b) ∩ ((ba) ∪ (ba))) ∪ ((a5 b) ∩ (ba )))
125, 7fh1 469 . . . . . 6 ((a5 b) ∩ ((ba) ∪ (ba))) = (((a5 b) ∩ (ba)) ∪ ((a5 b) ∩ (ba)))
13 ancom 74 . . . . . . . . 9 ((a5 b) ∩ (ba)) = ((ba) ∩ (a5 b))
14 ancom 74 . . . . . . . . . . 11 (ba) = (ab)
15 df-i5 48 . . . . . . . . . . . 12 (a5 b) = (((ab) ∪ (ab)) ∪ (ab ))
16 ax-a3 32 . . . . . . . . . . . 12 (((ab) ∪ (ab)) ∪ (ab )) = ((ab) ∪ ((ab) ∪ (ab )))
1715, 16ax-r2 36 . . . . . . . . . . 11 (a5 b) = ((ab) ∪ ((ab) ∪ (ab )))
1814, 172an 79 . . . . . . . . . 10 ((ba) ∩ (a5 b)) = ((ab) ∩ ((ab) ∪ ((ab) ∪ (ab ))))
19 anabs 121 . . . . . . . . . 10 ((ab) ∩ ((ab) ∪ ((ab) ∪ (ab )))) = (ab)
2018, 19ax-r2 36 . . . . . . . . 9 ((ba) ∩ (a5 b)) = (ab)
2113, 20ax-r2 36 . . . . . . . 8 ((a5 b) ∩ (ba)) = (ab)
22 anandi 114 . . . . . . . . 9 ((a5 b) ∩ (ba)) = (((a5 b) ∩ b ) ∩ ((a5 b) ∩ a))
23 u5lemanb 619 . . . . . . . . . . 11 ((a5 b) ∩ b ) = (ab )
24 u5lemaa 604 . . . . . . . . . . 11 ((a5 b) ∩ a) = (ab)
2523, 242an 79 . . . . . . . . . 10 (((a5 b) ∩ b ) ∩ ((a5 b) ∩ a)) = ((ab ) ∩ (ab))
26 ancom 74 . . . . . . . . . . 11 ((ab ) ∩ (ab)) = ((ab) ∩ (ab ))
27 an4 86 . . . . . . . . . . . 12 ((ab) ∩ (ab )) = ((aa ) ∩ (bb ))
28 dff 101 . . . . . . . . . . . . . . 15 0 = (bb )
2928ax-r1 35 . . . . . . . . . . . . . 14 (bb ) = 0
3029lan 77 . . . . . . . . . . . . 13 ((aa ) ∩ (bb )) = ((aa ) ∩ 0)
31 an0 108 . . . . . . . . . . . . 13 ((aa ) ∩ 0) = 0
3230, 31ax-r2 36 . . . . . . . . . . . 12 ((aa ) ∩ (bb )) = 0
3327, 32ax-r2 36 . . . . . . . . . . 11 ((ab) ∩ (ab )) = 0
3426, 33ax-r2 36 . . . . . . . . . 10 ((ab ) ∩ (ab)) = 0
3525, 34ax-r2 36 . . . . . . . . 9 (((a5 b) ∩ b ) ∩ ((a5 b) ∩ a)) = 0
3622, 35ax-r2 36 . . . . . . . 8 ((a5 b) ∩ (ba)) = 0
3721, 362or 72 . . . . . . 7 (((a5 b) ∩ (ba)) ∪ ((a5 b) ∩ (ba))) = ((ab) ∪ 0)
38 or0 102 . . . . . . 7 ((ab) ∪ 0) = (ab)
3937, 38ax-r2 36 . . . . . 6 (((a5 b) ∩ (ba)) ∪ ((a5 b) ∩ (ba))) = (ab)
4012, 39ax-r2 36 . . . . 5 ((a5 b) ∩ ((ba) ∪ (ba))) = (ab)
41 ancom 74 . . . . . 6 ((a5 b) ∩ (ba )) = ((ba ) ∩ (a5 b))
42 ancom 74 . . . . . . . 8 (ba ) = (ab )
43 ax-a2 31 . . . . . . . . 9 (((ab) ∪ (ab)) ∪ (ab )) = ((ab ) ∪ ((ab) ∪ (ab)))
4415, 43ax-r2 36 . . . . . . . 8 (a5 b) = ((ab ) ∪ ((ab) ∪ (ab)))
4542, 442an 79 . . . . . . 7 ((ba ) ∩ (a5 b)) = ((ab ) ∩ ((ab ) ∪ ((ab) ∪ (ab))))
46 anabs 121 . . . . . . 7 ((ab ) ∩ ((ab ) ∪ ((ab) ∪ (ab)))) = (ab )
4745, 46ax-r2 36 . . . . . 6 ((ba ) ∩ (a5 b)) = (ab )
4841, 47ax-r2 36 . . . . 5 ((a5 b) ∩ (ba )) = (ab )
4940, 482or 72 . . . 4 (((a5 b) ∩ ((ba) ∪ (ba))) ∪ ((a5 b) ∩ (ba ))) = ((ab) ∪ (ab ))
50 id 59 . . . 4 ((ab) ∪ (ab )) = ((ab) ∪ (ab ))
5149, 50ax-r2 36 . . 3 (((a5 b) ∩ ((ba) ∪ (ba))) ∪ ((a5 b) ∩ (ba ))) = ((ab) ∪ (ab ))
5211, 51ax-r2 36 . 2 ((a5 b) ∩ (((ba) ∪ (ba)) ∪ (ba ))) = ((ab) ∪ (ab ))
53 df-i5 48 . . 3 (b5 a) = (((ba) ∪ (ba)) ∪ (ba ))
5453lan 77 . 2 ((a5 b) ∩ (b5 a)) = ((a5 b) ∩ (((ba) ∪ (ba)) ∪ (ba )))
55 dfb 94 . 2 (ab) = ((ab) ∪ (ab ))
5652, 54, 553tr1 63 1 ((a5 b) ∩ (b5 a)) = (ab)
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  0wf 9   →5 wi5 16 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-i5 48  df-le1 130  df-le2 131  df-c1 132  df-c2 133 This theorem is referenced by:  oago3.21x  890
 Copyright terms: Public domain W3C validator