Theorem sylbbr

Description: A mixed syllogism inference from two biconditionals.

Note on the various syllogism-like statements in set.mm. The hypothetical syllogism syl infers an implication from two implications (and there are 3syl and 4syl for chaining more inferences). There are four inferences inferring an implication from one implication and one biconditional: sylbi , sylib , sylbir , sylibr ; four inferences inferring an implication from two biconditionals: sylbb , sylbbr , sylbb1 , sylbb2 ; four inferences inferring a biconditional from two biconditionals: bitri , bitr2i , bitr3i , bitr4i (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld , syl5 , syl6 , mpbid , bitrd , bitrid , bitrdi and variants. (Contributed by BJ, 21-Apr-2019)

	Ref	Expression
Hypotheses	sylbbr.1	⊢ ( 𝜑 ↔ 𝜓 )
	sylbbr.2	⊢ ( 𝜓 ↔ 𝜒 )
Assertion	sylbbr	⊢ ( 𝜒 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sylbbr.1	⊢ ( 𝜑 ↔ 𝜓 )
2		sylbbr.2	⊢ ( 𝜓 ↔ 𝜒 )
3	2	biimpri	⊢ ( 𝜒 → 𝜓 )
4	3 1	sylibr	⊢ ( 𝜒 → 𝜑 )