Theorem sylanblrc

Description: Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019)

	Ref	Expression
Hypotheses	sylanblrc.1	|- ( ph -> ps )
	sylanblrc.2	|- ch
	sylanblrc.3	|- ( th <-> ( ps /\ ch ) )
Assertion	sylanblrc	|- ( ph -> th )

Proof

Step	Hyp	Ref	Expression
1		sylanblrc.1	|- ( ph -> ps )
2		sylanblrc.2	|- ch
3		sylanblrc.3	|- ( th <-> ( ps /\ ch ) )
4	2	a1i	|- ( ph -> ch )
5	1 4 3	sylanbrc	|- ( ph -> th )