Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Natural addition
nadd42
Next ⟩
naddel12
Metamath Proof Explorer
Ascii
Unicode
Theorem
nadd42
Description:
Rearragement of terms in a quadruple sum.
(Contributed by
Scott Fenton
, 5-Feb-2025)
Ref
Expression
Assertion
nadd42
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
B
+
C
+
D
=
A
+
C
+
D
+
B
Proof
Step
Hyp
Ref
Expression
1
nadd4
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
B
+
C
+
D
=
A
+
C
+
B
+
D
2
naddcom
⊢
B
∈
On
∧
D
∈
On
→
B
+
D
=
D
+
B
3
2
ad2ant2l
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
B
+
D
=
D
+
B
4
3
oveq2d
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
C
+
B
+
D
=
A
+
C
+
D
+
B
5
1
4
eqtrd
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
D
∈
On
→
A
+
B
+
C
+
D
=
A
+
C
+
D
+
B