Metamath Proof Explorer


Theorem 2p4e6

Description: 2 + 4 = 6. (Contributed by SN, 24-Aug-2026)

Ref Expression
Assertion 2p4e6 2 + 4 = 6

Proof

Step Hyp Ref Expression
1 2cn 2
2 1 1 1 addassi 2 + 2 + 2 = 2 + 2 + 2
3 2p2e4 2 + 2 = 4
4 3 oveq1i 2 + 2 + 2 = 4 + 2
5 4p2e6 4 + 2 = 6
6 4 5 eqtri 2 + 2 + 2 = 6
7 3 oveq2i 2 + 2 + 2 = 2 + 4
8 2 6 7 3eqtr3ri 2 + 4 = 6