Metamath Proof Explorer

Theorem 2sqreulem3

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

		Ref	Expression
	Assertion	2sqreulem3	$⊢ (A \in ℕ_{0} \land (B \in ℕ_{0} \land C \in ℕ_{0})) \to (((φ \land A^{2} + B^{2} = P) \land (ψ \land A^{2} + C^{2} = P)) \to B = C)$

Proof

Step	Hyp	Ref	Expression
1		eqeq2	$⊢ P = A^{2} + B^{2} \to (A^{2} + C^{2} = P \leftrightarrow A^{2} + C^{2} = A^{2} + B^{2})$
2	1	eqcoms	$⊢ A^{2} + B^{2} = P \to (A^{2} + C^{2} = P \leftrightarrow A^{2} + C^{2} = A^{2} + B^{2})$
3	2	adantl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land C \in ℕ_{0}) \land A^{2} + B^{2} = P) \to (A^{2} + C^{2} = P \leftrightarrow A^{2} + C^{2} = A^{2} + B^{2})$
4		eqcom	$⊢ A^{2} + C^{2} = A^{2} + B^{2} \leftrightarrow A^{2} + B^{2} = A^{2} + C^{2}$
5		2sqreulem2	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land C \in ℕ_{0}) \to (A^{2} + B^{2} = A^{2} + C^{2} \to B = C)$
6	4 5	biimtrid	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land C \in ℕ_{0}) \to (A^{2} + C^{2} = A^{2} + B^{2} \to B = C)$
7	6	adantr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land C \in ℕ_{0}) \land A^{2} + B^{2} = P) \to (A^{2} + C^{2} = A^{2} + B^{2} \to B = C)$
8	3 7	sylbid	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land C \in ℕ_{0}) \land A^{2} + B^{2} = P) \to (A^{2} + C^{2} = P \to B = C)$
9	8	adantld	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land C \in ℕ_{0}) \land A^{2} + B^{2} = P) \to ((ψ \land A^{2} + C^{2} = P) \to B = C)$
10	9	ex	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land C \in ℕ_{0}) \to (A^{2} + B^{2} = P \to ((ψ \land A^{2} + C^{2} = P) \to B = C))$
11	10	adantld	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land C \in ℕ_{0}) \to ((φ \land A^{2} + B^{2} = P) \to ((ψ \land A^{2} + C^{2} = P) \to B = C))$
12	11	impd	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land C \in ℕ_{0}) \to (((φ \land A^{2} + B^{2} = P) \land (ψ \land A^{2} + C^{2} = P)) \to B = C)$
13	12	3expb	$⊢ (A \in ℕ_{0} \land (B \in ℕ_{0} \land C \in ℕ_{0})) \to (((φ \land A^{2} + B^{2} = P) \land (ψ \land A^{2} + C^{2} = P)) \to B = C)$