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

Theorem u21lembi 727
 Description: Dishkant/Sasaki implication and biconditional. (Contributed by NM, 3-Mar-2000.)
Assertion
Ref Expression
u21lembi ((a2 b) ∩ (b1 a)) = (ab)

Proof of Theorem u21lembi
StepHypRef Expression
1 u2lemc1 681 . . . . 5 b C (a2 b)
21comcom3 454 . . . 4 b C (a2 b)
3 comanr1 464 . . . . 5 b C (ba)
43comcom3 454 . . . 4 b C (ba)
52, 4fh2 470 . . 3 ((a2 b) ∩ (b ∪ (ba))) = (((a2 b) ∩ b ) ∪ ((a2 b) ∩ (ba)))
6 u2lemanb 616 . . . 4 ((a2 b) ∩ b ) = (ab )
7 u2lemab 611 . . . . . 6 ((a2 b) ∩ b) = b
87ran 78 . . . . 5 (((a2 b) ∩ b) ∩ a) = (ba)
9 anass 76 . . . . 5 (((a2 b) ∩ b) ∩ a) = ((a2 b) ∩ (ba))
10 ancom 74 . . . . 5 (ba) = (ab)
118, 9, 103tr2 64 . . . 4 ((a2 b) ∩ (ba)) = (ab)
126, 112or 72 . . 3 (((a2 b) ∩ b ) ∪ ((a2 b) ∩ (ba))) = ((ab ) ∪ (ab))
13 ax-a2 31 . . 3 ((ab ) ∪ (ab)) = ((ab) ∪ (ab ))
145, 12, 133tr 65 . 2 ((a2 b) ∩ (b ∪ (ba))) = ((ab) ∪ (ab ))
15 df-i1 44 . . 3 (b1 a) = (b ∪ (ba))
1615lan 77 . 2 ((a2 b) ∩ (b1 a)) = ((a2 b) ∩ (b ∪ (ba)))
17 dfb 94 . 2 (ab) = ((ab) ∪ (ab ))
1814, 16, 173tr1 63 1 ((a2 b) ∩ (b1 a)) = (ab)
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7   →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: (None)
 Copyright terms: Public domain W3C validator