Theorem sylbbr 238

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 219, sylib 220, sylbir 237, sylibr 236; four inferences inferring an implication from two biconditionals: sylbb 221, sylbbr 238, sylbb1 239, sylbb2 240; four inferences inferring a biconditional from two biconditionals: bitri 277, bitr2i 278, bitr3i 279, bitr4i 280 (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 234, bitrd 281, bitrid 285, bitrdi 289 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 230	. 2 ⊢ (𝜒 → 𝜓)
3		sylbbr.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	sylibr 236	1 ⊢ (𝜒 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bitri  277  euelss  4285  dfnfc2  4888  ndmima  6092  unfi  9139  axcclem  10425  cshw1  14845  fsumcom2  15811  fprodcom2  16024  pmtr3ncomlem1  19523  mdetunilem7  22685  cmpcov2  23457  hausflf2  24065  conway  27879  umgredg  29346  vtxdginducedm1  29751  2pthfrgrrn  30491  eqdif  32724  padct  32926  cusgredgex2  35478  f1omptsnlem  37835  igenval2  38570  mpobi123f  38666  dmqsblocks  39471  brtrclfv2  44308  clsk1indlem3  44624  permaxpow  45576  permaxpr  45577  or2expropbilem1  47617  grtriproplem  48552  mo0sn  49428