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  4664  ftpg  7155  frrlem13  8296  brinxper  8725  sdom0  9098  funsnfsupp  9353  sucprcreg  9569  sucprcregOLD  9570  fin23lem40  10336  ffz0iswrd  14580  s4f1o  14957  fsumsplitsnun  15808  lcmcllem  16655  catcone0  17744  prmidl2  21447  lidldvgen  21483  mat1dimbas  22610  pmatcollpw3fi  22923  nbgrssvwo2  29693  wlkn0  29951  clwlkcompbp  30112  clwlkclwwlkflem  30336  konigsberglem5  30588  difininv  32844  eulerpartlemgs2  34751  bnj1476  35216  bnj1204  35381  axprALT2  35484  noinfepregs  35527  dfon2lem3  36256  bj-ccinftydisj  37838  nninfnub  38383  ispridl2  38670  rp-isfinite6  44227  fnresfnco  47761