Metamath Proof Explorer


Theorem eel0000

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

Proof

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