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  4721  ftpg  7190  frrlem13  8339  wfrlem5OLD  8369  brinxper  8792  sdom0  9174  funsnfsupp  9461  sucprcreg  9670  fin23lem40  10420  ffz0iswrd  14589  s4f1o  14967  fsumsplitsnun  15803  lcmcllem  16643  catcone0  17745  lidldvgen  21367  mat1dimbas  22499  pmatcollpw3fi  22812  nbgrssvwo2  29397  wlkn0  29657  clwlkcompbp  29818  clwlkclwwlkflem  30036  konigsberglem5  30288  difininv  32547  prmidl2  33434  eulerpartlemgs2  34345  bnj1476  34823  bnj1204  34988  dfon2lem3  35749  bj-ccinftydisj  37179  nninfnub  37711  ispridl2  37998  rp-isfinite6  43480  fnresfnco  46956