Theorem syl3an12

Description: A double syllogism inference. (Contributed by SN, 15-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		syl3an12.1	|- ( ph -> ps )
2		syl3an12.2	|- ( ch -> th )
3		syl3an12.s	|- ( ( ps /\ th /\ ta ) -> et )
4		id	|- ( ta -> ta )
5	1 2 4 3	syl3an	|- ( ( ph /\ ch /\ ta ) -> et )