Theorem inass | index | src |

theorem inass (A B C: set): $ A i^i B i^i C == A i^i (B i^i C) $;
StepHypRefExpression
1 bitr4
(x e. A i^i B i^i C <-> x e. A i^i B /\ x e. C) -> (x e. A i^i (B i^i C) <-> x e. A i^i B /\ x e. C) -> (x e. A i^i B i^i C <-> x e. A i^i (B i^i C))
2 elin
x e. A i^i B i^i C <-> x e. A i^i B /\ x e. C
3 1, 2 ax_mp
(x e. A i^i (B i^i C) <-> x e. A i^i B /\ x e. C) -> (x e. A i^i B i^i C <-> x e. A i^i (B i^i C))
4 bitr4
(x e. A i^i (B i^i C) <-> x e. A /\ x e. B i^i C) -> (x e. A i^i B /\ x e. C <-> x e. A /\ x e. B i^i C) -> (x e. A i^i (B i^i C) <-> x e. A i^i B /\ x e. C)
5 elin
x e. A i^i (B i^i C) <-> x e. A /\ x e. B i^i C
6 4, 5 ax_mp
(x e. A i^i B /\ x e. C <-> x e. A /\ x e. B i^i C) -> (x e. A i^i (B i^i C) <-> x e. A i^i B /\ x e. C)
7 bitr4
(x e. A i^i B /\ x e. C <-> x e. A /\ x e. B /\ x e. C) ->
  (x e. A /\ x e. B i^i C <-> x e. A /\ x e. B /\ x e. C) ->
  (x e. A i^i B /\ x e. C <-> x e. A /\ x e. B i^i C)
8 elin
x e. A i^i B <-> x e. A /\ x e. B
9 8 aneq1i
x e. A i^i B /\ x e. C <-> x e. A /\ x e. B /\ x e. C
10 7, 9 ax_mp
(x e. A /\ x e. B i^i C <-> x e. A /\ x e. B /\ x e. C) -> (x e. A i^i B /\ x e. C <-> x e. A /\ x e. B i^i C)
11 bitr4
(x e. A /\ x e. B i^i C <-> x e. A /\ (x e. B /\ x e. C)) ->
  (x e. A /\ x e. B /\ x e. C <-> x e. A /\ (x e. B /\ x e. C)) ->
  (x e. A /\ x e. B i^i C <-> x e. A /\ x e. B /\ x e. C)
12 elin
x e. B i^i C <-> x e. B /\ x e. C
13 12 aneq2i
x e. A /\ x e. B i^i C <-> x e. A /\ (x e. B /\ x e. C)
14 11, 13 ax_mp
(x e. A /\ x e. B /\ x e. C <-> x e. A /\ (x e. B /\ x e. C)) -> (x e. A /\ x e. B i^i C <-> x e. A /\ x e. B /\ x e. C)
15 anass
x e. A /\ x e. B /\ x e. C <-> x e. A /\ (x e. B /\ x e. C)
16 14, 15 ax_mp
x e. A /\ x e. B i^i C <-> x e. A /\ x e. B /\ x e. C
17 10, 16 ax_mp
x e. A i^i B /\ x e. C <-> x e. A /\ x e. B i^i C
18 6, 17 ax_mp
x e. A i^i (B i^i C) <-> x e. A i^i B /\ x e. C
19 3, 18 ax_mp
x e. A i^i B i^i C <-> x e. A i^i (B i^i C)
20 19 eqri
A i^i B i^i C == A i^i (B i^i C)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8)