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

Theorem ud3lem1 570
 Description: Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
Assertion
Ref Expression
ud3lem1 ((a3 b) →3 (b3 a)) = (a ∪ (ab ))

Proof of Theorem ud3lem1
StepHypRef Expression
1 df-i3 46 . 2 ((a3 b) →3 (b3 a)) = ((((a3 b) ∩ (b3 a)) ∪ ((a3 b) ∩ (b3 a) )) ∪ ((a3 b) ∩ ((a3 b) ∪ (b3 a))))
2 ud3lem1a 566 . . . . . 6 ((a3 b) ∩ (b3 a)) = (ab )
3 ud3lem1b 567 . . . . . 6 ((a3 b) ∩ (b3 a) ) = 0
42, 32or 72 . . . . 5 (((a3 b) ∩ (b3 a)) ∪ ((a3 b) ∩ (b3 a) )) = ((ab ) ∪ 0)
5 or0 102 . . . . 5 ((ab ) ∪ 0) = (ab )
64, 5ax-r2 36 . . . 4 (((a3 b) ∩ (b3 a)) ∪ ((a3 b) ∩ (b3 a) )) = (ab )
7 ud3lem1d 569 . . . 4 ((a3 b) ∩ ((a3 b) ∪ (b3 a))) = ((ab ) ∪ (a ∩ (ab)))
86, 72or 72 . . 3 ((((a3 b) ∩ (b3 a)) ∪ ((a3 b) ∩ (b3 a) )) ∪ ((a3 b) ∩ ((a3 b) ∪ (b3 a)))) = ((ab ) ∪ ((ab ) ∪ (a ∩ (ab))))
9 coman1 185 . . . . . . 7 (ab ) C a
109comcom2 183 . . . . . . . 8 (ab ) C a
11 coman2 186 . . . . . . . . 9 (ab ) C b
1211comcom7 460 . . . . . . . 8 (ab ) C b
1310, 12com2or 483 . . . . . . 7 (ab ) C (ab)
149, 13fh3 471 . . . . . 6 ((ab ) ∪ (a ∩ (ab))) = (((ab ) ∪ a) ∩ ((ab ) ∪ (ab)))
15 ax-a2 31 . . . . . . . . 9 ((ab ) ∪ a) = (a ∪ (ab ))
16 orabs 120 . . . . . . . . 9 (a ∪ (ab )) = a
1715, 16ax-r2 36 . . . . . . . 8 ((ab ) ∪ a) = a
18 ax-a2 31 . . . . . . . . 9 ((ab ) ∪ (ab)) = ((ab) ∪ (ab ))
19 anor1 88 . . . . . . . . . . 11 (ab ) = (ab)
2019lor 70 . . . . . . . . . 10 ((ab) ∪ (ab )) = ((ab) ∪ (ab) )
21 df-t 41 . . . . . . . . . . 11 1 = ((ab) ∪ (ab) )
2221ax-r1 35 . . . . . . . . . 10 ((ab) ∪ (ab) ) = 1
2320, 22ax-r2 36 . . . . . . . . 9 ((ab) ∪ (ab )) = 1
2418, 23ax-r2 36 . . . . . . . 8 ((ab ) ∪ (ab)) = 1
2517, 242an 79 . . . . . . 7 (((ab ) ∪ a) ∩ ((ab ) ∪ (ab))) = (a ∩ 1)
26 an1 106 . . . . . . 7 (a ∩ 1) = a
2725, 26ax-r2 36 . . . . . 6 (((ab ) ∪ a) ∩ ((ab ) ∪ (ab))) = a
2814, 27ax-r2 36 . . . . 5 ((ab ) ∪ (a ∩ (ab))) = a
2928lor 70 . . . 4 ((ab ) ∪ ((ab ) ∪ (a ∩ (ab)))) = ((ab ) ∪ a)
30 or12 80 . . . 4 ((ab ) ∪ ((ab ) ∪ (a ∩ (ab)))) = ((ab ) ∪ ((ab ) ∪ (a ∩ (ab))))
31 ax-a2 31 . . . 4 (a ∪ (ab )) = ((ab ) ∪ a)
3229, 30, 313tr1 63 . . 3 ((ab ) ∪ ((ab ) ∪ (a ∩ (ab)))) = (a ∪ (ab ))
338, 32ax-r2 36 . 2 ((((a3 b) ∩ (b3 a)) ∪ ((a3 b) ∩ (b3 a) )) ∪ ((a3 b) ∩ ((a3 b) ∪ (b3 a)))) = (a ∪ (ab ))
341, 33ax-r2 36 1 ((a3 b) →3 (b3 a)) = (a ∪ (ab ))
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →3 wi3 14 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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133 This theorem is referenced by:  ud3  597  u3lem11a  787
 Copyright terms: Public domain W3C validator