Theorem sylbb2 238

Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.)

Hypotheses

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

Assertion

Ref	Expression
sylbb2	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbb2

Step	Hyp	Ref	Expression
1		sylbb2.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		sylbb2.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	biimpri 228	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	sylbi 217	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  rexprg  4697  ftpg  7176  frrlem13  8323  wfrlem5OLD  8353  brinxper  8774  sdom0  9148  funsnfsupp  9432  sucprcreg  9641  fin23lem40  10391  ffz0iswrd  14579  s4f1o  14957  fsumsplitsnun  15791  lcmcllem  16633  catcone0  17730  lidldvgen  21344  mat1dimbas  22478  pmatcollpw3fi  22791  nbgrssvwo2  29379  wlkn0  29639  clwlkcompbp  29802  clwlkclwwlkflem  30023  konigsberglem5  30275  difininv  32536  prmidl2  33469  eulerpartlemgs2  34382  bnj1476  34861  bnj1204  35026  dfon2lem3  35786  bj-ccinftydisj  37214  nninfnub  37758  ispridl2  38045  rp-isfinite6  43531  fnresfnco  47053