Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Natural addition
nadd4
Next ⟩
nadd42
Metamath Proof Explorer
Ascii
Unicode
Theorem
nadd4
Description:
Rearragement of terms in a quadruple sum.
(Contributed by
Scott Fenton
, 5-Feb-2025)
Ref
Expression
Assertion
nadd4
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
B
+
C
+
D
=
A
+
C
+
B
+
D
Proof
Step
Hyp
Ref
Expression
1
nadd32
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
→
A
+
B
+
C
=
A
+
C
+
B
2
1
3expa
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
→
A
+
B
+
C
=
A
+
C
+
B
3
2
adantrr
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
B
+
C
=
A
+
C
+
B
4
3
oveq1d
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
B
+
C
+
D
=
A
+
C
+
B
+
D
5
naddcl
⊢
A
∈
On
∧
B
∈
On
→
A
+
B
∈
On
6
5
adantr
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
B
∈
On
7
simprl
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
C
∈
On
8
simprr
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
D
∈
On
9
naddass
⊢
A
+
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
B
+
C
+
D
=
A
+
B
+
C
+
D
10
6
7
8
9
syl3anc
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
B
+
C
+
D
=
A
+
B
+
C
+
D
11
naddcl
⊢
A
∈
On
∧
C
∈
On
→
A
+
C
∈
On
12
11
ad2ant2r
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
C
∈
On
13
simplr
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
B
∈
On
14
naddass
⊢
A
+
C
∈
On
∧
B
∈
On
∧
D
∈
On
→
A
+
C
+
B
+
D
=
A
+
C
+
B
+
D
15
12
13
8
14
syl3anc
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
C
+
B
+
D
=
A
+
C
+
B
+
D
16
4
10
15
3eqtr3d
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
B
+
C
+
D
=
A
+
C
+
B
+
D