Description: Elimination rule similar to mp4an , except with a left-nested conjunction unification theorem. (Contributed by Alan Sare, 17-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eel0000.1 | |- ph |
|
eel0000.2 | |- ps |
||
eel0000.3 | |- ch |
||
eel0000.4 | |- th |
||
eel0000.5 | |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta ) |
||
Assertion | eel0000 | |- ta |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eel0000.1 | |- ph |
|
2 | eel0000.2 | |- ps |
|
3 | eel0000.3 | |- ch |
|
4 | eel0000.4 | |- th |
|
5 | eel0000.5 | |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta ) |
|
6 | 5 | exp41 | |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) ) |
7 | 1 2 6 | mp2 | |- ( ch -> ( th -> ta ) ) |
8 | 3 4 7 | mp2 | |- ta |