Description: Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009) (Proof shortened by Mario Carneiro, 11-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subtr.1 | |
|
subtr.2 | |
||
subtr.3 | |
||
subtr.4 | |
||
subtr.5 | |
||
subtr.6 | |
||
Assertion | subtr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subtr.1 | |
|
2 | subtr.2 | |
|
3 | subtr.3 | |
|
4 | subtr.4 | |
|
5 | subtr.5 | |
|
6 | subtr.6 | |
|
7 | 1 2 | nfeq | |
8 | 3 4 | nfeq | |
9 | 7 8 | nfim | |
10 | eqeq1 | |
|
11 | 5 | eqeq1d | |
12 | 10 11 | imbi12d | |
13 | 1 9 12 6 | vtoclgf | |
14 | 13 | adantr | |