Metamath Proof Explorer


Theorem axprlem4OLD

Description: Obsolete version of axprlem4 as of 18-Sep-2025. (Contributed by Rohan Ridenour, 10-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axprlem4OLD s n s t ¬ t n s p w = x s s p if- n n s w = x w = y

Proof

Step Hyp Ref Expression
1 axprlem1 s n t ¬ t n n s
2 1 bm1.3iiOLD s n n s t ¬ t n
3 nfa1 s s n s t ¬ t n s p
4 nfv s w = x
5 3 4 nfan s s n s t ¬ t n s p w = x
6 biimp n s t ¬ t n n s t ¬ t n
7 6 alimi n n s t ¬ t n n n s t ¬ t n
8 df-ral n s t ¬ t n n n s t ¬ t n
9 7 8 sylibr n n s t ¬ t n n s t ¬ t n
10 sp s n s t ¬ t n s p n s t ¬ t n s p
11 9 10 mpan9 n n s t ¬ t n s n s t ¬ t n s p s p
12 11 adantrr n n s t ¬ t n s n s t ¬ t n s p w = x s p
13 ax-nul n t ¬ t n
14 nfa1 n n n s t ¬ t n
15 sp n n s t ¬ t n n s t ¬ t n
16 15 biimprd n n s t ¬ t n t ¬ t n n s
17 14 16 eximd n n s t ¬ t n n t ¬ t n n n s
18 13 17 mpi n n s t ¬ t n n n s
19 simprr n n s t ¬ t n s n s t ¬ t n s p w = x w = x
20 ifptru n n s if- n n s w = x w = y w = x
21 20 biimpar n n s w = x if- n n s w = x w = y
22 18 19 21 syl2an2r n n s t ¬ t n s n s t ¬ t n s p w = x if- n n s w = x w = y
23 12 22 jca n n s t ¬ t n s n s t ¬ t n s p w = x s p if- n n s w = x w = y
24 23 expcom s n s t ¬ t n s p w = x n n s t ¬ t n s p if- n n s w = x w = y
25 5 24 eximd s n s t ¬ t n s p w = x s n n s t ¬ t n s s p if- n n s w = x w = y
26 2 25 mpi s n s t ¬ t n s p w = x s s p if- n n s w = x w = y