Metamath Proof Explorer

Theorem 2sqreulem3

Description: Lemma 3 for 2sqreu etc. (Contributed by AV, 25-Jun-2023)

Ref Expression
Assertion 2sqreulem3 ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 → φ ∧ A 2 + B 2 = P ∧ ψ ∧ A 2 + C 2 = P → B = C

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ P = A 2 + B 2 → A 2 + C 2 = P ↔ A 2 + C 2 = A 2 + B 2
2 1 eqcoms ⊢ A 2 + B 2 = P → A 2 + C 2 = P ↔ A 2 + C 2 = A 2 + B 2
3 2 adantl ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A 2 + B 2 = P → A 2 + C 2 = P ↔ A 2 + C 2 = A 2 + B 2
4 eqcom ⊢ A 2 + C 2 = A 2 + B 2 ↔ A 2 + B 2 = A 2 + C 2
5 2sqreulem2 ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 → A 2 + B 2 = A 2 + C 2 → B = C
6 4 5 syl5bi ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 → A 2 + C 2 = A 2 + B 2 → B = C
7 6 adantr ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A 2 + B 2 = P → A 2 + C 2 = A 2 + B 2 → B = C
8 3 7 sylbid ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A 2 + B 2 = P → A 2 + C 2 = P → B = C
9 8 adantld ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A 2 + B 2 = P → ψ ∧ A 2 + C 2 = P → B = C
10 9 ex ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 → A 2 + B 2 = P → ψ ∧ A 2 + C 2 = P → B = C
11 10 adantld ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 → φ ∧ A 2 + B 2 = P → ψ ∧ A 2 + C 2 = P → B = C
12 11 impd ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 → φ ∧ A 2 + B 2 = P ∧ ψ ∧ A 2 + C 2 = P → B = C
13 12 3expb ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 → φ ∧ A 2 + B 2 = P ∧ ψ ∧ A 2 + C 2 = P → B = C