Description: Deduction for membership in the class of homotopies. (Contributed by Mario Carneiro, 22-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ishtpy.1 | |
|
ishtpy.3 | |
||
ishtpy.4 | |
||
ishtpyd.1 | |
||
ishtpyd.2 | |
||
ishtpyd.3 | |
||
Assertion | ishtpyd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ishtpy.1 | |
|
2 | ishtpy.3 | |
|
3 | ishtpy.4 | |
|
4 | ishtpyd.1 | |
|
5 | ishtpyd.2 | |
|
6 | ishtpyd.3 | |
|
7 | 5 6 | jca | |
8 | 7 | ralrimiva | |
9 | 1 2 3 | ishtpy | |
10 | 4 8 9 | mpbir2and | |