Theorem eel12131

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

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

Proof

Step	Hyp	Ref	Expression
1		eel12131.1	|- ( ph -> ps )
2		eel12131.2	|- ( ( ph /\ ch ) -> th )
3		eel12131.3	|- ( ( ph /\ ta ) -> et )
4		eel12131.4	|- ( ( ps /\ th /\ et ) -> ze )
5	4	3exp	|- ( ps -> ( th -> ( et -> ze ) ) )
6	1 2 5	syl2imc	|- ( ( ph /\ ch ) -> ( ph -> ( et -> ze ) ) )
7	6	ex	|- ( ph -> ( ch -> ( ph -> ( et -> ze ) ) ) )
8	7	pm2.43b	|- ( ch -> ( ph -> ( et -> ze ) ) )
9	8	com13	|- ( et -> ( ph -> ( ch -> ze ) ) )
10	3 9	syl	|- ( ( ph /\ ta ) -> ( ph -> ( ch -> ze ) ) )
11	10	ex	|- ( ph -> ( ta -> ( ph -> ( ch -> ze ) ) ) )
12	11	pm2.43b	|- ( ta -> ( ph -> ( ch -> ze ) ) )
13	12	3imp231	|- ( ( ph /\ ch /\ ta ) -> ze )