Quantum Logic Explorer This is the Unicode version. Change to GIF version

 Ref Expression (see link for any distinct variable requirements) wb 1 wff  a = b wle 2 wff  a ≤ b wc 3 wff  a C b wn 4 term  a⊥ tb 5 term  (a ≡ b) wo 6 term  (a ∪ b) wa 7 term  (a ∩ b) wt 8 term  1 wf 9 term  0 wle2 10 term  (a ≤2 b) wi0 11 term  (a →0 b) wi1 12 term  (a →1 b) wi2 13 term  (a →2 b) wi3 14 term  (a →3 b) wi4 15 term  (a →4 b) wi5 16 term  (a →5 b) wid0 17 term  (a ≡0 b) wid1 18 term  (a ≡1 b) wid2 19 term  (a ≡2 b) wid3 20 term  (a ≡3 b) wid4 21 term  (a ≡4 b) wid5 22 term  (a ≡5 b) wb3 23 term  (a ↔3 b) wb1 24 term  (a ↔1 b) wo3 25 term  (a ∪3 b) wan3 26 term  (a ∩3 b) wid3oa 27 term  (a ≡ c ≡OA b) wid4oa 28 term  (a ≡ c, d ≡OA b) wcmtr 29 term  C (a, b) ax-a1 30 a = a⊥ ⊥ ax-a2 31 (a ∪ b) = (b ∪ a) ax-a3 32 ((a ∪ b) ∪ c) = (a ∪ (b ∪ c)) ax-a4 33 (a ∪ (b ∪ b⊥ )) = (b ∪ b⊥ ) ax-a5 34 (a ∪ (a⊥ ∪ b)⊥ ) = a ax-r1 35 a = b    ⇒   b = a ax-r2 36 a = b    &   b = c    ⇒   a = c ax-r4 37 a = b    ⇒   a⊥ = b⊥ ax-r5 38 a = b    ⇒   (a ∪ c) = (b ∪ c) df-b 39 (a ≡ b) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ ) df-a 40 (a ∩ b) = (a⊥ ∪ b⊥ )⊥ df-t 41 1 = (a ∪ a⊥ ) df-f 42 0 = 1⊥ df-i0 43 (a →0 b) = (a⊥ ∪ b) df-i1 44 (a →1 b) = (a⊥ ∪ (a ∩ b)) df-i2 45 (a →2 b) = (b ∪ (a⊥ ∩ b⊥ )) df-i3 46 (a →3 b) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) df-i4 47 (a →4 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ )) df-i5 48 (a →5 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) df-id0 49 (a ≡0 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ a)) df-id1 50 (a ≡1 b) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ b))) df-id2 51 (a ≡2 b) = ((a ∪ b⊥ ) ∩ (b ∪ (a⊥ ∩ b⊥ ))) df-id3 52 (a ≡3 b) = ((a⊥ ∪ b) ∩ (a ∪ (a⊥ ∩ b⊥ ))) df-id4 53 (a ≡4 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ (a ∩ b))) df-o3 54 (a ∪3 b) = (a⊥ →3 (a⊥ →3 b)) df-a3 55 (a ∩3 b) = (a⊥ ∪3 b⊥ )⊥ df-b3 56 (a ↔3 b) = ((a →3 b) ∩ (b →3 a)) df-id3oa 57 (a ≡ c ≡OA b) = (((a →1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c))) df-id4oa 58 (a ≡ c, d ≡OA b) = ((a ≡ d ≡OA b) ∪ ((a ≡ d ≡OA c) ∩ (b ≡ d ≡OA c))) df-le 129 (a ≤2 b) = ((a ∪ b) ≡ b) df-le1 130 (a ∪ b) = b    ⇒   a ≤ b df-le2 131 a ≤ b    ⇒   (a ∪ b) = b df-c1 132 a = ((a ∩ b) ∪ (a ∩ b⊥ ))    ⇒   a C b df-c2 133 a C b    ⇒   a = ((a ∩ b) ∪ (a ∩ b⊥ )) df-cmtr 134 C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) ax-wom 361 (a⊥ ∪ (a ∩ b)) = 1    ⇒   (b ∪ (a⊥ ∩ b⊥ )) = 1 ax-r3 439 (c ∪ c⊥ ) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )    ⇒   a = b ax-oadist 994 e = (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))))    &   f = (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ e)    &   h ≤ (a →1 d)    &   j ≤ f    &   k ≤ f    &   (h ∩ (b →1 d)) ≤ k    ⇒   (h ∩ (j ∪ k)) = ((h ∩ j) ∪ (h ∩ k)) ax-3oa 998 ((a →1 c) ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c) ax-oal4 1026 a ≤ b⊥    &   c ≤ d⊥    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ (b ∪ (a ∩ (c ∪ ((a ∪ c) ∩ (b ∪ d))))) ax-oa6 1030 a ≤ b⊥    &   c ≤ d⊥    &   e ≤ f⊥    ⇒   (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f))))))) ax-4oa 1033 ((a →1 d) ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d)))))) ≤ (b →1 d) ax-newstateeq 1045 (((a →1 b) →1 (c →1 b)) ∩ ((a →1 c) ∩ (b →1 a))) ≤ (c →1 a) df-id5 1047 (a ≡5 b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ )) df-b1 1048 (a ↔1 b) = ((a →1 b) ∩ (b →1 a)) ax-wdol 1102 ((a ≡ b) ∪ (a ≡ b⊥ )) = 1 ax-ml 1120 ((a ∪ b) ∩ (a ∪ c)) ≤ (a ∪ (b ∩ (a ∪ c))) ax-arg 1151 ((a0 ∪ b0) ∩ (a1 ∪ b1)) ≤ (a2 ∪ b2)    ⇒   ((a0 ∪ a1) ∩ (b0 ∪ b1)) ≤ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2)))
 Copyright terms: Public domain W3C validator