Theorem sylbb2 239

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 229	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	sylbi 218	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  rexprg  4636  ftpg  7106  frrlem13  8245  brinxper  8670  sdom0  9044  funsnfsupp  9302  sucprcreg  9518  sucprcregOLD  9519  fin23lem40  10271  ffz0iswrd  14501  s4f1o  14878  fsumsplitsnun  15715  lcmcllem  16563  catcone0  17651  lidldvgen  21334  mat1dimbas  22462  pmatcollpw3fi  22775  nbgrssvwo2  29456  wlkn0  29714  clwlkcompbp  29875  clwlkclwwlkflem  30099  konigsberglem5  30351  difininv  32612  prmidl2  33531  eulerpartlemgs2  34571  bnj1476  35036  bnj1204  35201  axprALT2  35297  noinfepregs  35321  dfon2lem3  36018  bj-ccinftydisj  37580  nninfnub  38125  ispridl2  38412  rp-isfinite6  43969  fnresfnco  47511