Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 11-May-1993) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbv2h.1 | |
|
cbv2h.2 | |
||
cbv2h.3 | |
||
Assertion | cbv2h | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbv2h.1 | |
|
2 | cbv2h.2 | |
|
3 | cbv2h.3 | |
|
4 | biimp | |
|
5 | 3 4 | syl6 | |
6 | 1 2 5 | cbv1h | |
7 | equcomi | |
|
8 | biimpr | |
|
9 | 7 3 8 | syl56 | |
10 | 2 1 9 | cbv1h | |
11 | 10 | alcoms | |
12 | 6 11 | impbid | |