Description: Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eel11111.1 | |- ( ph -> ps ) |
|
eel11111.2 | |- ( ph -> ch ) |
||
eel11111.3 | |- ( ph -> th ) |
||
eel11111.4 | |- ( ph -> ta ) |
||
eel11111.5 | |- ( ph -> et ) |
||
eel11111.6 | |- ( ( ( ( ( ps /\ ch ) /\ th ) /\ ta ) /\ et ) -> ze ) |
||
Assertion | eel11111 | |- ( ph -> ze ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eel11111.1 | |- ( ph -> ps ) |
|
2 | eel11111.2 | |- ( ph -> ch ) |
|
3 | eel11111.3 | |- ( ph -> th ) |
|
4 | eel11111.4 | |- ( ph -> ta ) |
|
5 | eel11111.5 | |- ( ph -> et ) |
|
6 | eel11111.6 | |- ( ( ( ( ( ps /\ ch ) /\ th ) /\ ta ) /\ et ) -> ze ) |
|
7 | 6 | exp41 | |- ( ( ps /\ ch ) -> ( th -> ( ta -> ( et -> ze ) ) ) ) |
8 | 7 | ex | |- ( ps -> ( ch -> ( th -> ( ta -> ( et -> ze ) ) ) ) ) |
9 | 1 2 3 8 | syl3c | |- ( ph -> ( ta -> ( et -> ze ) ) ) |
10 | 4 5 9 | mp2d | |- ( ph -> ze ) |