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

Theorem 3vroa 831
Description: OA-like inference rule (requires OM only). (Contributed by NM, 13-Nov-1998.)
Hypothesis
Ref Expression
3vroa.1 ((a2 b) ∩ ((bc) →0 ((a2 b) ∩ (a2 c)))) = 1
Assertion
Ref Expression
3vroa (a2 c) = 1

Proof of Theorem 3vroa
StepHypRef Expression
1 df-i2 45 . 2 (a2 c) = (c ∪ (ac ))
2 or12 80 . . 3 (c ∪ ((ac ) ∪ (ac ))) = ((ac ) ∪ (c ∪ (ac )))
3 oridm 110 . . . 4 ((ac ) ∪ (ac )) = (ac )
43lor 70 . . 3 (c ∪ ((ac ) ∪ (ac ))) = (c ∪ (ac ))
5 le1 146 . . . . . . . . . 10 (a2 b) ≤ 1
6 3vroa.1 . . . . . . . . . . . 12 ((a2 b) ∩ ((bc) →0 ((a2 b) ∩ (a2 c)))) = 1
76ax-r1 35 . . . . . . . . . . 11 1 = ((a2 b) ∩ ((bc) →0 ((a2 b) ∩ (a2 c))))
8 lea 160 . . . . . . . . . . 11 ((a2 b) ∩ ((bc) →0 ((a2 b) ∩ (a2 c)))) ≤ (a2 b)
97, 8bltr 138 . . . . . . . . . 10 1 ≤ (a2 b)
105, 9lebi 145 . . . . . . . . 9 (a2 b) = 1
1110ran 78 . . . . . . . 8 ((a2 b) ∩ (a2 c)) = (1 ∩ (a2 c))
12 ancom 74 . . . . . . . 8 (1 ∩ (a2 c)) = ((a2 c) ∩ 1)
1311, 12ax-r2 36 . . . . . . 7 ((a2 b) ∩ (a2 c)) = ((a2 c) ∩ 1)
14 an1 106 . . . . . . 7 ((a2 c) ∩ 1) = (a2 c)
1513, 14, 13tr 65 . . . . . 6 ((a2 b) ∩ (a2 c)) = (c ∪ (ac ))
1615lor 70 . . . . 5 ((ac ) ∪ ((a2 b) ∩ (a2 c))) = ((ac ) ∪ (c ∪ (ac )))
1716ax-r1 35 . . . 4 ((ac ) ∪ (c ∪ (ac ))) = ((ac ) ∪ ((a2 b) ∩ (a2 c)))
18 le1 146 . . . . 5 ((ac ) ∪ ((a2 b) ∩ (a2 c))) ≤ 1
19 lear 161 . . . . . . . 8 ((a2 b) ∩ ((bc) →0 ((a2 b) ∩ (a2 c)))) ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))
20 df-i0 43 . . . . . . . . 9 ((bc) →0 ((a2 b) ∩ (a2 c))) = ((bc) ∪ ((a2 b) ∩ (a2 c)))
21 anor3 90 . . . . . . . . . . 11 (bc ) = (bc)
2221ax-r5 38 . . . . . . . . . 10 ((bc ) ∪ ((a2 b) ∩ (a2 c))) = ((bc) ∪ ((a2 b) ∩ (a2 c)))
2322ax-r1 35 . . . . . . . . 9 ((bc) ∪ ((a2 b) ∩ (a2 c))) = ((bc ) ∪ ((a2 b) ∩ (a2 c)))
2420, 23ax-r2 36 . . . . . . . 8 ((bc) →0 ((a2 b) ∩ (a2 c))) = ((bc ) ∪ ((a2 b) ∩ (a2 c)))
2519, 6, 24le3tr2 141 . . . . . . 7 1 ≤ ((bc ) ∪ ((a2 b) ∩ (a2 c)))
26 le1 146 . . . . . . 7 ((bc ) ∪ ((a2 b) ∩ (a2 c))) ≤ 1
2725, 26lebi 145 . . . . . 6 1 = ((bc ) ∪ ((a2 b) ∩ (a2 c)))
2810u2lemle2 716 . . . . . . . . 9 ab
2928lecon 154 . . . . . . . 8 ba
3029leran 153 . . . . . . 7 (bc ) ≤ (ac )
3130leror 152 . . . . . 6 ((bc ) ∪ ((a2 b) ∩ (a2 c))) ≤ ((ac ) ∪ ((a2 b) ∩ (a2 c)))
3227, 31bltr 138 . . . . 5 1 ≤ ((ac ) ∪ ((a2 b) ∩ (a2 c)))
3318, 32lebi 145 . . . 4 ((ac ) ∪ ((a2 b) ∩ (a2 c))) = 1
3417, 33ax-r2 36 . . 3 ((ac ) ∪ (c ∪ (ac ))) = 1
352, 4, 343tr2 64 . 2 (c ∪ (ac )) = 1
361, 35ax-r2 36 1 (a2 c) = 1
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  0 wi0 11  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-i0 43  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