Metamath Proof Explorer


Theorem prtlem17

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 15-Oct-2010)

Ref Expression
Assertion prtlem17 PrtAxAzxyAzywywx

Proof

Step Hyp Ref Expression
1 df-rex yAzywyyyAzywy
2 an32 xAyAzxxAzxyA
3 prtlem14 PrtAxAyAzxzyx=y
4 elequ2 x=ywxwy
5 4 biimprd x=ywywx
6 3 5 syl8 PrtAxAyAzxzywywx
7 6 exp4a PrtAxAyAzxzywywx
8 7 impd PrtAxAyAzxzywywx
9 2 8 syl5bir PrtAxAzxyAzywywx
10 9 expd PrtAxAzxyAzywywx
11 10 imp5a PrtAxAzxyAzywywx
12 11 imp4b PrtAxAzxyAzywywx
13 12 exlimdv PrtAxAzxyyAzywywx
14 1 13 syl5bi PrtAxAzxyAzywywx
15 14 ex PrtAxAzxyAzywywx