Theorem 4p4e8ALT 43128

Description: A shorter proof of 4p4e8 12422 if 6p2e8 12426 was moved up. The most clean way to do this would be to start with 7p2e9 12428, then go 6p2e8 12426, 6p3e9 12427, etc., which is still inelegant. The idea here is that using 4 = 2 + 2 and 2cn 12343 is shorter than using 4 = 3 + 1, 3cn 12349, and ax-1cn 11185. This also works with 5p4e9 12425. (Contributed by SN, 24-Aug-2026.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
4p4e8ALT	⊢ (4 + 4) = 8

Proof of Theorem 4p4e8ALT

Step	Hyp	Ref	Expression
1		4cn 12353	. . 3 ⊢ 4 ∈ ℂ
2		2cn 12343	. . 3 ⊢ 2 ∈ ℂ
3	1, 2, 2	addassi 11246	. 2 ⊢ ((4 + 2) + 2) = (4 + (2 + 2))
4		4p2e6 12420	. . . 4 ⊢ (4 + 2) = 6
5	4	oveq1i 7424	. . 3 ⊢ ((4 + 2) + 2) = (6 + 2)
6		6p2e8 12426	. . 3 ⊢ (6 + 2) = 8
7	5, 6	eqtri 2783	. 2 ⊢ ((4 + 2) + 2) = 8
8		2p2e4 12402	. . 3 ⊢ (2 + 2) = 4
9	8	oveq2i 7425	. 2 ⊢ (4 + (2 + 2)) = (4 + 4)
10	3, 7, 9	3eqtr3ri 2792	1 ⊢ (4 + 4) = 8

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7414   + caddc 11130  2c2 12322  4c4 12324  6c6 12326  8c8 12328

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11185  ax-addcl 11187  ax-addass 11192

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336

This theorem is used by: (None)