Theorem sylbb2 241

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  rexprg  4659  ftpg  7143  frrlem13  8283  brinxper  8712  sdom0  9085  funsnfsupp  9340  sucprcreg  9556  sucprcregOLD  9557  fin23lem40  10323  ffz0iswrd  14568  s4f1o  14945  fsumsplitsnun  15796  lcmcllem  16644  catcone0  17733  prmidl2  21428  lidldvgen  21462  mat1dimbas  22590  pmatcollpw3fi  22903  nbgrssvwo2  29621  wlkn0  29879  clwlkcompbp  30040  clwlkclwwlkflem  30264  konigsberglem5  30516  difininv  32773  eulerpartlemgs2  34687  bnj1476  35152  bnj1204  35317  axprALT2  35417  noinfepregs  35441  dfon2lem3  36146  bj-ccinftydisj  37717  nninfnub  38262  ispridl2  38549  rp-isfinite6  44106  fnresfnco  47633