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  27301  umgredg  28429  vtxdginducedm1  28831  2pthfrgrrn  29566  eqdif  31788  cusgredgex2  34144  f1omptsnlem  36265  igenval2  36982  mpobi123f  37078  brtrclfv2  42526  clsk1indlem3  42842  or2expropbilem1  45790  mo0sn  47548