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  4664  ftpg  7131  frrlem13  8280  brinxper  8703  sdom0  9079  funsnfsupp  9350  sucprcreg  9561  fin23lem40  10311  ffz0iswrd  14513  s4f1o  14891  fsumsplitsnun  15728  lcmcllem  16573  catcone0  17655  lidldvgen  21251  mat1dimbas  22366  pmatcollpw3fi  22679  nbgrssvwo2  29296  wlkn0  29556  clwlkcompbp  29719  clwlkclwwlkflem  29940  konigsberglem5  30192  difininv  32453  prmidl2  33419  eulerpartlemgs2  34378  bnj1476  34844  bnj1204  35009  dfon2lem3  35780  bj-ccinftydisj  37208  nninfnub  37752  ispridl2  38039  rp-isfinite6  43514  fnresfnco  47046