Theorem sylbbr 136

Description: A mixed syllogism inference from two biconditionals.

Note on the various syllogism-like statements in set.mm. The hypothetical syllogism syl 14 infers an implication from two implications (and there are 3syl 17 and 4syl 18 for chaining more inferences). There are four inferences inferring an implication from one implication and one biconditional: sylbi 121, sylib 122, sylbir 135, sylibr 134; four inferences inferring an implication from two biconditionals: sylbb 123, sylbbr 136, sylbb1 137, sylbb2 138; four inferences inferring a biconditional from two biconditionals: bitri 184, bitr2i 185, bitr3i 186, bitr4i 187 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 45, syl5 32, syl6 33, mpbid 147, bitrd 188, bitrid 192, bitrdi 196 and variants. (Contributed by BJ, 21-Apr-2019.)

Hypotheses

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

Assertion

Ref	Expression
sylbbr	⊢ (𝜒 → 𝜑)

Proof of Theorem sylbbr

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

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fisumcom2  11603  fprodcom2fi  11791