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

Theorem 2vwomlem 365
 Description: Lemma from 2-variable WOML rule.
Hypotheses
Ref Expression
2vwomlem.1 (a2 b) = 1
2vwomlem.2 (b2 a) = 1
Assertion
Ref Expression
2vwomlem (ab) = 1

Proof of Theorem 2vwomlem
StepHypRef Expression
1 dfb 94 . 2 (ab) = ((ab) ∪ (ab ))
2 df-f 42 . . . . 5 0 = 1
3 anor2 89 . . . . . . 7 (a ∩ (ab)) = (a ∪ (ab) )
43ax-r1 35 . . . . . 6 (a ∪ (ab) ) = (a ∩ (ab))
5 anor3 90 . . . . . . . . . . 11 (ab ) = (ab)
65ax-r1 35 . . . . . . . . . 10 (ab) = (ab )
7 ancom 74 . . . . . . . . . 10 (ab ) = (ba )
86, 7ax-r2 36 . . . . . . . . 9 (ab) = (ba )
98lor 70 . . . . . . . 8 (a ∪ (ab) ) = (a ∪ (ba ))
10 df-i2 45 . . . . . . . . 9 (b2 a) = (a ∪ (ba ))
1110ax-r1 35 . . . . . . . 8 (a ∪ (ba )) = (b2 a)
12 2vwomlem.2 . . . . . . . 8 (b2 a) = 1
139, 11, 123tr 65 . . . . . . 7 (a ∪ (ab) ) = 1
1413ax-r4 37 . . . . . 6 (a ∪ (ab) ) = 1
15 anabs 121 . . . . . . . . 9 (a ∩ (ab )) = a
1615ax-r1 35 . . . . . . . 8 a = (a ∩ (ab ))
1716ran 78 . . . . . . 7 (a ∩ (ab)) = ((a ∩ (ab )) ∩ (ab))
18 anass 76 . . . . . . 7 ((a ∩ (ab )) ∩ (ab)) = (a ∩ ((ab ) ∩ (ab)))
19 oran3 93 . . . . . . . . . 10 (ab ) = (ab)
20 oran 87 . . . . . . . . . 10 (ab) = (ab )
2119, 202an 79 . . . . . . . . 9 ((ab ) ∩ (ab)) = ((ab) ∩ (ab ) )
22 anor3 90 . . . . . . . . 9 ((ab) ∩ (ab ) ) = ((ab) ∪ (ab ))
2321, 22ax-r2 36 . . . . . . . 8 ((ab ) ∩ (ab)) = ((ab) ∪ (ab ))
2423lan 77 . . . . . . 7 (a ∩ ((ab ) ∩ (ab))) = (a ∩ ((ab) ∪ (ab )) )
2517, 18, 243tr 65 . . . . . 6 (a ∩ (ab)) = (a ∩ ((ab) ∪ (ab )) )
264, 14, 253tr2 64 . . . . 5 1 = (a ∩ ((ab) ∪ (ab )) )
272, 26ax-r2 36 . . . 4 0 = (a ∩ ((ab) ∪ (ab )) )
2827lor 70 . . 3 (((ab) ∪ (ab )) ∪ 0) = (((ab) ∪ (ab )) ∪ (a ∩ ((ab) ∪ (ab )) ))
29 or0 102 . . 3 (((ab) ∪ (ab )) ∪ 0) = ((ab) ∪ (ab ))
30 le1 146 . . . . 5 (a ∪ (a ∩ ((ab) ∪ (ab )))) ≤ 1
31 df-i2 45 . . . . . . . . . 10 (a2 b) = (b ∪ (ab ))
3231ax-r1 35 . . . . . . . . 9 (b ∪ (ab )) = (a2 b)
33 2vwomlem.1 . . . . . . . . 9 (a2 b) = 1
3432, 33ax-r2 36 . . . . . . . 8 (b ∪ (ab )) = 1
35342vwomr2 362 . . . . . . 7 (a ∪ (ab)) = 1
3635ax-r1 35 . . . . . 6 1 = (a ∪ (ab))
37 lea 160 . . . . . . . 8 (ab) ≤ a
38 leo 158 . . . . . . . 8 (ab) ≤ ((ab) ∪ (ab ))
3937, 38ler2an 173 . . . . . . 7 (ab) ≤ (a ∩ ((ab) ∪ (ab )))
4039lelor 166 . . . . . 6 (a ∪ (ab)) ≤ (a ∪ (a ∩ ((ab) ∪ (ab ))))
4136, 40bltr 138 . . . . 5 1 ≤ (a ∪ (a ∩ ((ab) ∪ (ab ))))
4230, 41lebi 145 . . . 4 (a ∪ (a ∩ ((ab) ∪ (ab )))) = 1
4342ax-wom 361 . . 3 (((ab) ∪ (ab )) ∪ (a ∩ ((ab) ∪ (ab )) )) = 1
4428, 29, 433tr2 64 . 2 ((ab) ∪ (ab )) = 1
451, 44ax-r2 36 1 (ab) = 1
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →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-wom 361 This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i2 45  df-le1 130  df-le2 131 This theorem is referenced by:  wr5-2v  366
 Copyright terms: Public domain W3C validator