Theorem sylbir

Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-1993)

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

Proof

Step	Hyp	Ref	Expression
1		sylbir.1	|- ( ps <-> ph )
2		sylbir.2	|- ( ps -> ch )
3	1	biimpri	|- ( ph -> ps )
4	3 2	syl	|- ( ph -> ch )