sn-addcan2d

	Ref	Expression
Hypotheses	sn-addcan2d.a	$⊢ φ \to A \in ℂ$
	sn-addcan2d.b	$⊢ φ \to B \in ℂ$
	sn-addcan2d.c	$⊢ φ \to C \in ℂ$
Assertion	sn-addcan2d	$⊢ φ \to (A + C = B + C \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		sn-addcan2d.a	$⊢ φ \to A \in ℂ$
2		sn-addcan2d.b	$⊢ φ \to B \in ℂ$
3		sn-addcan2d.c	$⊢ φ \to C \in ℂ$
4		sn-negex	$⊢ C \in ℂ \to \exists x \in ℂ C + x = 0$
5	3 4	syl	$⊢ φ \to \exists x \in ℂ C + x = 0$
6		oveq1	$⊢ A + C = B + C \to A + C + x = B + C + x$
7	1	adantr	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to A \in ℂ$
8	3	adantr	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to C \in ℂ$
9		simprl	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to x \in ℂ$
10	7 8 9	addassd	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to A + C + x = A + C + x$
11		simprr	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to C + x = 0$
12	11	oveq2d	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to A + C + x = A + 0$
13		sn-addrid	$⊢ A \in ℂ \to A + 0 = A$
14	7 13	syl	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to A + 0 = A$
15	10 12 14	3eqtrd	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to A + C + x = A$
16	2	adantr	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to B \in ℂ$
17	16 8 9	addassd	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to B + C + x = B + C + x$
18	11	oveq2d	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to B + C + x = B + 0$
19		sn-addrid	$⊢ B \in ℂ \to B + 0 = B$
20	16 19	syl	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to B + 0 = B$
21	17 18 20	3eqtrd	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to B + C + x = B$
22	15 21	eqeq12d	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to (A + C + x = B + C + x \leftrightarrow A = B)$
23	6 22	imbitrid	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to (A + C = B + C \to A = B)$
24		oveq1	$⊢ A = B \to A + C = B + C$
25	23 24	impbid1	$⊢ (φ \land (x \in ℂ \land C + x = 0)) \to (A + C = B + C \leftrightarrow A = B)$
26	5 25	rexlimddv	$⊢ φ \to (A + C = B + C \leftrightarrow A = B)$

Metamath Proof Explorer

Theorem sn-addcan2d

Proof