Theorem sylbb

Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019)

	Ref	Expression
Hypotheses	sylbb.1	|- ( ph <-> ps )
	sylbb.2	|- ( ps <-> ch )
Assertion	sylbb	|- ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		sylbb.1	|- ( ph <-> ps )
2		sylbb.2	|- ( ps <-> ch )
3	2	biimpi	|- ( ps -> ch )
4	1 3	sylbi	|- ( ph -> ch )