Theorem 3imp3i2an

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017) (Proof shortened by Wolf Lammen, 13-Apr-2022)

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

Proof

Step	Hyp	Ref	Expression
1		3imp3i2an.1	|- ( ( ph /\ ps /\ ch ) -> th )
2		3imp3i2an.2	|- ( ( ph /\ ch ) -> ta )
3		3imp3i2an.3	|- ( ( th /\ ta ) -> et )
4	2	3adant2	|- ( ( ph /\ ps /\ ch ) -> ta )
5	1 4 3	syl2anc	|- ( ( ph /\ ps /\ ch ) -> et )