Metamath Proof Explorer


Theorem axprlem3

Description: Lemma for axpr . Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023) (Proof shortened by Matthew House, 18-Sep-2025)

Ref Expression
Assertion axprlem3 z w w z s s p if- n n s w = x w = y

Proof

Step Hyp Ref Expression
1 axrep4v s z w if- n n s w = x w = y w = z z w w z s s p if- n n s w = x w = y
2 ifptru n n s if- n n s w = x w = y w = x
3 2 biimpd n n s if- n n s w = x w = y w = x
4 equeuclr z = x w = x w = z
5 3 4 syl9r z = x n n s if- n n s w = x w = y w = z
6 5 alrimdv z = x n n s w if- n n s w = x w = y w = z
7 6 spimevw n n s z w if- n n s w = x w = y w = z
8 ifpfal ¬ n n s if- n n s w = x w = y w = y
9 8 biimpd ¬ n n s if- n n s w = x w = y w = y
10 equeuclr z = y w = y w = z
11 9 10 syl9r z = y ¬ n n s if- n n s w = x w = y w = z
12 11 alrimdv z = y ¬ n n s w if- n n s w = x w = y w = z
13 12 spimevw ¬ n n s z w if- n n s w = x w = y w = z
14 7 13 pm2.61i z w if- n n s w = x w = y w = z
15 1 14 mpg z w w z s s p if- n n s w = x w = y