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 274, bitr2i 275, bitr3i 276, bitr4i 277 (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 278, syl5bb 282, bitrdi 286 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  274  euelss  4260  dfnfc2  4868  ndmima  6008  unfi  8920  axcclem  10197  cshw1  14516  fsumcom2  15467  fprodcom2  15675  pmtr3ncomlem1  19062  mdetunilem7  21748  cmpcov2  22522  hausflf2  23130  umgredg  27489  vtxdginducedm1  27891  2pthfrgrrn  28625  eqdif  30845  cusgredgex2  33063  conway  33972  f1omptsnlem  35486  igenval2  36203  mpobi123f  36299  brtrclfv2  41288  clsk1indlem3  41606  or2expropbilem1  44477  mo0sn  46113