Metamath Proof Explorer


Theorem axprlem5OLD

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 axprlem5OLD s n s t ¬ t n s p w = y s s p if- n n s w = x w = y

Proof

Step Hyp Ref Expression
1 ax-nul s n ¬ n s
2 nfa1 s s n s t ¬ t n s p
3 nfv s w = y
4 2 3 nfan s s n s t ¬ t n s p w = y
5 pm2.21 ¬ n s n s t ¬ t n
6 5 alimi n ¬ n s n n s t ¬ t n
7 6 adantr n ¬ n s s n s t ¬ t n s p w = y 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 s n s t ¬ t n s p w = y n s t ¬ t n
10 sp s n s t ¬ t n s p n s t ¬ t n s p
11 10 ad2antrl n ¬ n s s n s t ¬ t n s p w = y n s t ¬ t n s p
12 9 11 mpd n ¬ n s s n s t ¬ t n s p w = y s p
13 simpl n ¬ n s s n s t ¬ t n s p w = y n ¬ n s
14 alnex n ¬ n s ¬ n n s
15 13 14 sylib n ¬ n s s n s t ¬ t n s p w = y ¬ n n s
16 simprr n ¬ n s s n s t ¬ t n s p w = y w = y
17 ifpfal ¬ n n s if- n n s w = x w = y w = y
18 17 biimpar ¬ n n s w = y if- n n s w = x w = y
19 15 16 18 syl2anc n ¬ n s s n s t ¬ t n s p w = y if- n n s w = x w = y
20 12 19 jca n ¬ n s s n s t ¬ t n s p w = y s p if- n n s w = x w = y
21 20 expcom s n s t ¬ t n s p w = y n ¬ n s s p if- n n s w = x w = y
22 4 21 eximd s n s t ¬ t n s p w = y s n ¬ n s s s p if- n n s w = x w = y
23 1 22 mpi s n s t ¬ t n s p w = y s s p if- n n s w = x w = y