Theorem sylbbr 235

Description: A mixed syllogism inference from two biconditionals.

Note on the various syllogism-like statements in set.mm. The hypothetical syllogism syl 17 infers an implication from two implications (and there are 3syl 18 and 4syl 19 for chaining more inferences). There are four inferences inferring an implication from one implication and one biconditional: sylbi 216, sylib 217, sylbir 234, sylibr 233; four inferences inferring an implication from two biconditionals: sylbb 218, sylbbr 235, sylbb1 236, sylbb2 237; four inferences inferring a biconditional from two biconditionals: bitri 275, bitr2i 276, bitr3i 277, bitr4i 278 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 47, syl5 34, syl6 35, mpbid 231, bitrd 279, bitrid 283, bitrdi 287 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 227	. 2 ⊢ (𝜒 → 𝜓)
3		sylbbr.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	sylibr 233	1 ⊢ (𝜒 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  bitri  275  euelss  4322  dfnfc2  4934  ndmima  6103  unfi  9172  axcclem  10452  cshw1  14772  fsumcom2  15720  fprodcom2  15928  pmtr3ncomlem1  19341  mdetunilem7  22120  cmpcov2  22894  hausflf2  23502  conway  27300  umgredg  28398  vtxdginducedm1  28800  2pthfrgrrn  29535  eqdif  31757  cusgredgex2  34113  f1omptsnlem  36217  igenval2  36934  mpobi123f  37030  brtrclfv2  42478  clsk1indlem3  42794  or2expropbilem1  45742  mo0sn  47500