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

Theorem u4lemoa 623
Description: Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)
Assertion
Ref Expression
u4lemoa ((a4 b) ∪ a) = 1

Proof of Theorem u4lemoa
StepHypRef Expression
1 df-i4 47 . . 3 (a4 b) = (((ab) ∪ (ab)) ∪ ((ab) ∩ b ))
21ax-r5 38 . 2 ((a4 b) ∪ a) = ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∪ a)
3 ax-a3 32 . . 3 ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∪ a) = (((ab) ∪ (ab)) ∪ (((ab) ∩ b ) ∪ a))
4 comor1 461 . . . . . . . 8 (ab) C a
54comcom7 460 . . . . . . 7 (ab) C a
6 comor2 462 . . . . . . . 8 (ab) C b
76comcom2 183 . . . . . . 7 (ab) C b
85, 7fh4r 476 . . . . . 6 (((ab) ∩ b ) ∪ a) = (((ab) ∪ a) ∩ (ba))
9 or32 82 . . . . . . . . 9 ((ab) ∪ a) = ((aa) ∪ b)
10 ax-a2 31 . . . . . . . . . 10 ((aa) ∪ b) = (b ∪ (aa))
11 df-t 41 . . . . . . . . . . . . . 14 1 = (aa )
12 ax-a2 31 . . . . . . . . . . . . . 14 (aa ) = (aa)
1311, 12ax-r2 36 . . . . . . . . . . . . 13 1 = (aa)
1413lor 70 . . . . . . . . . . . 12 (b ∪ 1) = (b ∪ (aa))
1514ax-r1 35 . . . . . . . . . . 11 (b ∪ (aa)) = (b ∪ 1)
16 or1 104 . . . . . . . . . . 11 (b ∪ 1) = 1
1715, 16ax-r2 36 . . . . . . . . . 10 (b ∪ (aa)) = 1
1810, 17ax-r2 36 . . . . . . . . 9 ((aa) ∪ b) = 1
199, 18ax-r2 36 . . . . . . . 8 ((ab) ∪ a) = 1
2019ran 78 . . . . . . 7 (((ab) ∪ a) ∩ (ba)) = (1 ∩ (ba))
21 ancom 74 . . . . . . . 8 (1 ∩ (ba)) = ((ba) ∩ 1)
22 an1 106 . . . . . . . 8 ((ba) ∩ 1) = (ba)
2321, 22ax-r2 36 . . . . . . 7 (1 ∩ (ba)) = (ba)
2420, 23ax-r2 36 . . . . . 6 (((ab) ∪ a) ∩ (ba)) = (ba)
258, 24ax-r2 36 . . . . 5 (((ab) ∩ b ) ∪ a) = (ba)
2625lor 70 . . . 4 (((ab) ∪ (ab)) ∪ (((ab) ∩ b ) ∪ a)) = (((ab) ∪ (ab)) ∪ (ba))
27 ax-a3 32 . . . . 5 (((ab) ∪ (ab)) ∪ (ba)) = ((ab) ∪ ((ab) ∪ (ba)))
28 ax-a2 31 . . . . . . . 8 ((ab) ∪ (ba)) = ((ba) ∪ (ab))
29 ancom 74 . . . . . . . . . . 11 (ab) = (ba )
30 anor1 88 . . . . . . . . . . 11 (ba ) = (ba)
3129, 30ax-r2 36 . . . . . . . . . 10 (ab) = (ba)
3231lor 70 . . . . . . . . 9 ((ba) ∪ (ab)) = ((ba) ∪ (ba) )
33 df-t 41 . . . . . . . . . 10 1 = ((ba) ∪ (ba) )
3433ax-r1 35 . . . . . . . . 9 ((ba) ∪ (ba) ) = 1
3532, 34ax-r2 36 . . . . . . . 8 ((ba) ∪ (ab)) = 1
3628, 35ax-r2 36 . . . . . . 7 ((ab) ∪ (ba)) = 1
3736lor 70 . . . . . 6 ((ab) ∪ ((ab) ∪ (ba))) = ((ab) ∪ 1)
38 or1 104 . . . . . 6 ((ab) ∪ 1) = 1
3937, 38ax-r2 36 . . . . 5 ((ab) ∪ ((ab) ∪ (ba))) = 1
4027, 39ax-r2 36 . . . 4 (((ab) ∪ (ab)) ∪ (ba)) = 1
4126, 40ax-r2 36 . . 3 (((ab) ∪ (ab)) ∪ (((ab) ∩ b ) ∪ a)) = 1
423, 41ax-r2 36 . 2 ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∪ a) = 1
432, 42ax-r2 36 1 ((a4 b) ∪ a) = 1
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  4 wi4 15
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-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  u4lemnana  648
  Copyright terms: Public domain W3C validator