Theorem undir | index | src |

theorem undir (A B C: set): $ A i^i B u. C == (A u. C) i^i (B u. C) $;
StepHypRefExpression
1 eqstr4
A i^i B u. C == C u. A i^i B -> (A u. C) i^i (B u. C) == C u. A i^i B -> A i^i B u. C == (A u. C) i^i (B u. C)
2 uncom
A i^i B u. C == C u. A i^i B
3 1, 2 ax_mp
(A u. C) i^i (B u. C) == C u. A i^i B -> A i^i B u. C == (A u. C) i^i (B u. C)
4 eqstr4
(A u. C) i^i (B u. C) == (C u. A) i^i (C u. B) -> C u. A i^i B == (C u. A) i^i (C u. B) -> (A u. C) i^i (B u. C) == C u. A i^i B
5 ineq
A u. C == C u. A -> B u. C == C u. B -> (A u. C) i^i (B u. C) == (C u. A) i^i (C u. B)
6 uncom
A u. C == C u. A
7 5, 6 ax_mp
B u. C == C u. B -> (A u. C) i^i (B u. C) == (C u. A) i^i (C u. B)
8 uncom
B u. C == C u. B
9 7, 8 ax_mp
(A u. C) i^i (B u. C) == (C u. A) i^i (C u. B)
10 4, 9 ax_mp
C u. A i^i B == (C u. A) i^i (C u. B) -> (A u. C) i^i (B u. C) == C u. A i^i B
11 undi
C u. A i^i B == (C u. A) i^i (C u. B)
12 10, 11 ax_mp
(A u. C) i^i (B u. C) == C u. A i^i B
13 3, 12 ax_mp
A i^i B u. C == (A u. C) i^i (B u. 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)