Metamath Proof Explorer


Theorem eel11111

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 )

Proof

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 )