Theorem bj-syl66ib

Description: A mixed syllogism inference derived from imbitrdi . In addition to bj-dvelimdv1 , it can also shorten alexsubALTlem4 (4821>4812), supsrlem (2868>2863). (Contributed by BJ, 20-Oct-2021)

	Ref	Expression
Hypotheses	bj-syl66ib.1	|- ( ph -> ( ps -> th ) )
	bj-syl66ib.2	|- ( th -> ta )
	bj-syl66ib.3	|- ( ta <-> ch )
Assertion	bj-syl66ib	|- ( ph -> ( ps -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		bj-syl66ib.1	|- ( ph -> ( ps -> th ) )
2		bj-syl66ib.2	|- ( th -> ta )
3		bj-syl66ib.3	|- ( ta <-> ch )
4	1 2	syl6	|- ( ph -> ( ps -> ta ) )
5	4 3	imbitrdi	|- ( ph -> ( ps -> ch ) )