Metamath Proof Explorer


Theorem axprOLD

Description: Obsolete version of axpr as of 18-Sep-2025. (Contributed by NM, 14-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axprOLD z w w = x w = y w z

Proof

Step Hyp Ref Expression
1 axprlem3OLD z w w z s s p if- n n s w = x w = y
2 biimpr w z s s p if- n n s w = x w = y s s p if- n n s w = x w = y w z
3 2 alimi w w z s s p if- n n s w = x w = y w s s p if- n n s w = x w = y w z
4 1 3 eximii z w s s p if- n n s w = x w = y w z
5 axprlem4OLD s n s t ¬ t n s p w = x s s p if- n n s w = x w = y
6 axprlem5OLD s n s t ¬ t n s p w = y s s p if- n n s w = x w = y
7 5 6 jaodan s n s t ¬ t n s p w = x w = y s s p if- n n s w = x w = y
8 7 ex s n s t ¬ t n s p w = x w = y s s p if- n n s w = x w = y
9 8 imim1d s n s t ¬ t n s p s s p if- n n s w = x w = y w z w = x w = y w z
10 9 alimdv s n s t ¬ t n s p w s s p if- n n s w = x w = y w z w w = x w = y w z
11 10 eximdv s n s t ¬ t n s p z w s s p if- n n s w = x w = y w z z w w = x w = y w z
12 4 11 mpi s n s t ¬ t n s p z w w = x w = y w z
13 axprlem2 p s n s t ¬ t n s p
14 12 13 exlimiiv z w w = x w = y w z