Description: Theorem *10.55 in WhiteheadRussell p. 156. (Contributed by Andrew Salmon, 24-May-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | pm10.55 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exsimpl | |
|
2 | 1 | anim1i | |
3 | exintr | |
|
4 | 3 | imdistanri | |
5 | 2 4 | impbii | |