Description: A version of climmul using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | climmulf.1 | |
|
climmulf.2 | |
||
climmulf.3 | |
||
climmulf.4 | |
||
climmulf.5 | |
||
climmulf.6 | |
||
climmulf.7 | |
||
climmulf.8 | |
||
climmulf.9 | |
||
climmulf.10 | |
||
climmulf.11 | |
||
climmulf.12 | |
||
Assertion | climmulf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | climmulf.1 | |
|
2 | climmulf.2 | |
|
3 | climmulf.3 | |
|
4 | climmulf.4 | |
|
5 | climmulf.5 | |
|
6 | climmulf.6 | |
|
7 | climmulf.7 | |
|
8 | climmulf.8 | |
|
9 | climmulf.9 | |
|
10 | climmulf.10 | |
|
11 | climmulf.11 | |
|
12 | climmulf.12 | |
|
13 | nfcv | |
|
14 | 13 | nfel1 | |
15 | 1 14 | nfan | |
16 | 2 13 | nffv | |
17 | 16 | nfel1 | |
18 | 15 17 | nfim | |
19 | eleq1w | |
|
20 | 19 | anbi2d | |
21 | fveq2 | |
|
22 | 21 | eleq1d | |
23 | 20 22 | imbi12d | |
24 | 18 23 10 | chvarfv | |
25 | 3 13 | nffv | |
26 | 25 | nfel1 | |
27 | 15 26 | nfim | |
28 | fveq2 | |
|
29 | 28 | eleq1d | |
30 | 20 29 | imbi12d | |
31 | 27 30 11 | chvarfv | |
32 | 4 13 | nffv | |
33 | nfcv | |
|
34 | 16 33 25 | nfov | |
35 | 32 34 | nfeq | |
36 | 15 35 | nfim | |
37 | fveq2 | |
|
38 | 21 28 | oveq12d | |
39 | 37 38 | eqeq12d | |
40 | 20 39 | imbi12d | |
41 | 36 40 12 | chvarfv | |
42 | 5 6 7 8 9 24 31 41 | climmul | |