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  4641  ftpg  7110  frrlem13  8248  brinxper  8673  sdom0  9047  funsnfsupp  9305  sucprcreg  9520  sucprcregOLD  9521  fin23lem40  10273  ffz0iswrd  14503  s4f1o  14880  fsumsplitsnun  15717  lcmcllem  16565  catcone0  17653  lidldvgen  21332  mat1dimbas  22437  pmatcollpw3fi  22750  nbgrssvwo2  29431  wlkn0  29689  clwlkcompbp  29850  clwlkclwwlkflem  30074  konigsberglem5  30326  difininv  32587  prmidl2  33501  eulerpartlemgs2  34524  bnj1476  34989  bnj1204  35154  axprALT2  35253  noinfepregs  35277  dfon2lem3  35965  bj-ccinftydisj  37527  nninfnub  38072  ispridl2  38359  rp-isfinite6  43945  fnresfnco  47489