Metamath Proof Explorer


Theorem mpsyl4anc

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017)

Ref Expression
Hypotheses mpsyl4anc.1
|- ph
mpsyl4anc.2
|- ps
mpsyl4anc.3
|- ch
mpsyl4anc.4
|- ( th -> ta )
mpsyl4anc.5
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) -> et )
Assertion mpsyl4anc
|- ( th -> et )

Proof

Step Hyp Ref Expression
1 mpsyl4anc.1
 |-  ph
2 mpsyl4anc.2
 |-  ps
3 mpsyl4anc.3
 |-  ch
4 mpsyl4anc.4
 |-  ( th -> ta )
5 mpsyl4anc.5
 |-  ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) -> et )
6 1 a1i
 |-  ( th -> ph )
7 2 a1i
 |-  ( th -> ps )
8 3 a1i
 |-  ( th -> ch )
9 6 7 8 4 5 syl1111anc
 |-  ( th -> et )