Theorem psubaddv-P6-L1 807

Description: Lemma for psubaddv-P6 808.

Hypotheses

Ref	Expression
psubaddv-P6-L1.1	⊢ ([𝑤 / 𝑥] 𝑎 = 𝑡₁ ↔ 𝑎 = 𝑢₁)
psubaddv-P6-L1.2	⊢ ([𝑤 / 𝑥] 𝑏 = 𝑡₂ ↔ 𝑏 = 𝑢₂)

Assertion

Ref	Expression
psubaddv-P6-L1	⊢ (𝑥 = 𝑤 → (𝑐 = (𝑡₁ + 𝑡₂) ↔ 𝑐 = (𝑢₁ + 𝑢₂)))

Distinct variable groups:   𝑡₁,𝑎   𝑡₂,𝑎   𝑢₁,𝑎   𝑢₂,𝑎   𝑤,𝑎   𝑡₁,𝑏   𝑡₂,𝑏   𝑢₁,𝑏   𝑢₂,𝑏   𝑤,𝑏   𝑡₁,𝑐   𝑢₁,𝑐   𝑢₂,𝑐   𝑤,𝑐   𝑎,𝑏,𝑐,𝑥

Proof of Theorem psubaddv-P6-L1

Step	Hyp	Ref	Expression
1		rcp-NDASM1of3 195	. . . . . . . . 9 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → 𝑎 = 𝑡₁)
2	1	eqsym-P5 627	. . . . . . . 8 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → 𝑡₁ = 𝑎)
3		psubtoisub-P6 765	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝑎 = 𝑡₁ ↔ [𝑤 / 𝑥] 𝑎 = 𝑡₁))
4		psubaddv-P6-L1.1	. . . . . . . . . . . . 13 ⊢ ([𝑤 / 𝑥] 𝑎 = 𝑡₁ ↔ 𝑎 = 𝑢₁)
5	4	rcp-NDIMP0addall 207	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → ([𝑤 / 𝑥] 𝑎 = 𝑡₁ ↔ 𝑎 = 𝑢₁))
6	3, 5	bitrns-P3.33c 302	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑎 = 𝑡₁ ↔ 𝑎 = 𝑢₁))
7	6	rcp-NDIMP0addall 207	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂) → (𝑥 = 𝑤 → (𝑎 = 𝑡₁ ↔ 𝑎 = 𝑢₁)))
8	7	rcp-IMPIME2 528	. . . . . . . . 9 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → (𝑎 = 𝑡₁ ↔ 𝑎 = 𝑢₁))
9	1, 8	bimpf-P4 531	. . . . . . . 8 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → 𝑎 = 𝑢₁)
10	2, 9	eqtrns-P5 630	. . . . . . 7 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → 𝑡₁ = 𝑢₁)
11		rcp-NDASM2of3 196	. . . . . . . . 9 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → 𝑏 = 𝑡₂)
12	11	eqsym-P5 627	. . . . . . . 8 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → 𝑡₂ = 𝑏)
13		psubtoisub-P6 765	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝑏 = 𝑡₂ ↔ [𝑤 / 𝑥] 𝑏 = 𝑡₂))
14		psubaddv-P6-L1.2	. . . . . . . . . . . . 13 ⊢ ([𝑤 / 𝑥] 𝑏 = 𝑡₂ ↔ 𝑏 = 𝑢₂)
15	14	rcp-NDIMP0addall 207	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → ([𝑤 / 𝑥] 𝑏 = 𝑡₂ ↔ 𝑏 = 𝑢₂))
16	13, 15	bitrns-P3.33c 302	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑏 = 𝑡₂ ↔ 𝑏 = 𝑢₂))
17	16	rcp-NDIMP0addall 207	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂) → (𝑥 = 𝑤 → (𝑏 = 𝑡₂ ↔ 𝑏 = 𝑢₂)))
18	17	rcp-IMPIME2 528	. . . . . . . . 9 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → (𝑏 = 𝑡₂ ↔ 𝑏 = 𝑢₂))
19	11, 18	bimpf-P4 531	. . . . . . . 8 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → 𝑏 = 𝑢₂)
20	12, 19	eqtrns-P5 630	. . . . . . 7 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → 𝑡₂ = 𝑢₂)
21	10, 20	subaddd-P5 647	. . . . . 6 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → (𝑡₁ + 𝑡₂) = (𝑢₁ + 𝑢₂))
22	21	subeqr-P5 635	. . . . 5 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂ ∧ 𝑥 = 𝑤) → (𝑐 = (𝑡₁ + 𝑡₂) ↔ 𝑐 = (𝑢₁ + 𝑢₂)))
23	22	rcp-NDIMI3 225	. . . 4 ⊢ ((𝑎 = 𝑡₁ ∧ 𝑏 = 𝑡₂) → (𝑥 = 𝑤 → (𝑐 = (𝑡₁ + 𝑡₂) ↔ 𝑐 = (𝑢₁ + 𝑢₂))))
24	23	rcp-NDIMI2 224	. . 3 ⊢ (𝑎 = 𝑡₁ → (𝑏 = 𝑡₂ → (𝑥 = 𝑤 → (𝑐 = (𝑡₁ + 𝑡₂) ↔ 𝑐 = (𝑢₁ + 𝑢₂)))))
25		axL6ex-P5 625	. . 3 ⊢ ∃𝑎 𝑎 = 𝑡₁
26	24, 25	exiav-P5.SH 616	. 2 ⊢ (𝑏 = 𝑡₂ → (𝑥 = 𝑤 → (𝑐 = (𝑡₁ + 𝑡₂) ↔ 𝑐 = (𝑢₁ + 𝑢₂))))
27		axL6ex-P5 625	. 2 ⊢ ∃𝑏 𝑏 = 𝑡₂
28	26, 27	exiav-P5.SH 616	1 ⊢ (𝑥 = 𝑤 → (𝑐 = (𝑡₁ + 𝑡₂) ↔ 𝑐 = (𝑢₁ + 𝑢₂)))

Syntax hints:  term-obj 1   + term-add 4   = wff-equals 6   → wff-imp 10   ↔ wff-bi 104   ∧ wff-and 132   ∧ wff-rcp-AND3 160  [wff-psub 714

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L9-addl 23  ax-L9-addr 24  ax-L10 27  ax-L12 29

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682  df-psub-D6.2 716

This theorem is referenced by:  psubaddv-P6  808