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

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

Proof of Theorem u4lemona
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 or32 82 . . 3 ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∪ a ) = ((((ab) ∪ (ab)) ∪ a ) ∪ ((ab) ∩ b ))
4 ax-a3 32 . . . . . 6 (((ab) ∪ (ab)) ∪ a ) = ((ab) ∪ ((ab) ∪ a ))
5 lea 160 . . . . . . . 8 (ab) ≤ a
65df-le2 131 . . . . . . 7 ((ab) ∪ a ) = a
76lor 70 . . . . . 6 ((ab) ∪ ((ab) ∪ a )) = ((ab) ∪ a )
84, 7ax-r2 36 . . . . 5 (((ab) ∪ (ab)) ∪ a ) = ((ab) ∪ a )
98ax-r5 38 . . . 4 ((((ab) ∪ (ab)) ∪ a ) ∪ ((ab) ∩ b )) = (((ab) ∪ a ) ∪ ((ab) ∩ b ))
10 comor1 461 . . . . . . . . 9 (ab) C a
1110comcom7 460 . . . . . . . 8 (ab) C a
12 comor2 462 . . . . . . . 8 (ab) C b
1311, 12com2an 484 . . . . . . 7 (ab) C (ab)
1413, 10com2or 483 . . . . . 6 (ab) C ((ab) ∪ a )
1512comcom2 183 . . . . . 6 (ab) C b
1614, 15fh4 472 . . . . 5 (((ab) ∪ a ) ∪ ((ab) ∩ b )) = ((((ab) ∪ a ) ∪ (ab)) ∩ (((ab) ∪ a ) ∪ b ))
17 lear 161 . . . . . . . . . 10 (ab) ≤ b
18 leor 159 . . . . . . . . . 10 b ≤ (ab)
1917, 18letr 137 . . . . . . . . 9 (ab) ≤ (ab)
20 leo 158 . . . . . . . . 9 a ≤ (ab)
2119, 20lel2or 170 . . . . . . . 8 ((ab) ∪ a ) ≤ (ab)
2221df-le2 131 . . . . . . 7 (((ab) ∪ a ) ∪ (ab)) = (ab)
23 ax-a3 32 . . . . . . . 8 (((ab) ∪ a ) ∪ b ) = ((ab) ∪ (ab ))
24 df-a 40 . . . . . . . . . . . 12 (ab) = (ab )
2524ax-r1 35 . . . . . . . . . . 11 (ab ) = (ab)
2625con3 68 . . . . . . . . . 10 (ab ) = (ab)
2726lor 70 . . . . . . . . 9 ((ab) ∪ (ab )) = ((ab) ∪ (ab) )
28 df-t 41 . . . . . . . . . 10 1 = ((ab) ∪ (ab) )
2928ax-r1 35 . . . . . . . . 9 ((ab) ∪ (ab) ) = 1
3027, 29ax-r2 36 . . . . . . . 8 ((ab) ∪ (ab )) = 1
3123, 30ax-r2 36 . . . . . . 7 (((ab) ∪ a ) ∪ b ) = 1
3222, 312an 79 . . . . . 6 ((((ab) ∪ a ) ∪ (ab)) ∩ (((ab) ∪ a ) ∪ b )) = ((ab) ∩ 1)
33 an1 106 . . . . . 6 ((ab) ∩ 1) = (ab)
3432, 33ax-r2 36 . . . . 5 ((((ab) ∪ a ) ∪ (ab)) ∩ (((ab) ∪ a ) ∪ b )) = (ab)
3516, 34ax-r2 36 . . . 4 (((ab) ∪ a ) ∪ ((ab) ∩ b )) = (ab)
369, 35ax-r2 36 . . 3 ((((ab) ∪ (ab)) ∪ a ) ∪ ((ab) ∩ b )) = (ab)
373, 36ax-r2 36 . 2 ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∪ a ) = (ab)
382, 37ax-r2 36 1 ((a4 b) ∪ a ) = (ab)
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:  u4lemnaa  643  u4lem5  764
  Copyright terms: Public domain W3C validator