Metamath Proof Explorer


Theorem climmulf

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 kφ
climmulf.2 _kF
climmulf.3 _kG
climmulf.4 _kH
climmulf.5 Z=M
climmulf.6 φM
climmulf.7 φFA
climmulf.8 φHX
climmulf.9 φGB
climmulf.10 φkZFk
climmulf.11 φkZGk
climmulf.12 φkZHk=FkGk
Assertion climmulf φHAB

Proof

Step Hyp Ref Expression
1 climmulf.1 kφ
2 climmulf.2 _kF
3 climmulf.3 _kG
4 climmulf.4 _kH
5 climmulf.5 Z=M
6 climmulf.6 φM
7 climmulf.7 φFA
8 climmulf.8 φHX
9 climmulf.9 φGB
10 climmulf.10 φkZFk
11 climmulf.11 φkZGk
12 climmulf.12 φkZHk=FkGk
13 nfcv _kj
14 13 nfel1 kjZ
15 1 14 nfan kφjZ
16 2 13 nffv _kFj
17 16 nfel1 kFj
18 15 17 nfim kφjZFj
19 eleq1w k=jkZjZ
20 19 anbi2d k=jφkZφjZ
21 fveq2 k=jFk=Fj
22 21 eleq1d k=jFkFj
23 20 22 imbi12d k=jφkZFkφjZFj
24 18 23 10 chvarfv φjZFj
25 3 13 nffv _kGj
26 25 nfel1 kGj
27 15 26 nfim kφjZGj
28 fveq2 k=jGk=Gj
29 28 eleq1d k=jGkGj
30 20 29 imbi12d k=jφkZGkφjZGj
31 27 30 11 chvarfv φjZGj
32 4 13 nffv _kHj
33 nfcv _k×
34 16 33 25 nfov _kFjGj
35 32 34 nfeq kHj=FjGj
36 15 35 nfim kφjZHj=FjGj
37 fveq2 k=jHk=Hj
38 21 28 oveq12d k=jFkGk=FjGj
39 37 38 eqeq12d k=jHk=FkGkHj=FjGj
40 20 39 imbi12d k=jφkZHk=FkGkφjZHj=FjGj
41 36 40 12 chvarfv φjZHj=FjGj
42 5 6 7 8 9 24 31 41 climmul φHAB