Theorem indir ≪ | index | src | ≫ 

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