Theorem sylbb2 240

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  rexprg  4631  ftpg  7102  frrlem13  8241  brinxper  8667  sdom0  9041  funsnfsupp  9299  sucprcreg  9515  sucprcregOLD  9516  fin23lem40  10269  ffz0iswrd  14498  s4f1o  14875  fsumsplitsnun  15712  lcmcllem  16560  catcone0  17648  lidldvgen  21330  mat1dimbas  22458  pmatcollpw3fi  22771  nbgrssvwo2  29451  wlkn0  29709  clwlkcompbp  29870  clwlkclwwlkflem  30094  konigsberglem5  30346  difininv  32607  prmidl2  33526  eulerpartlemgs2  34574  bnj1476  35042  bnj1204  35207  axprALT2  35303  noinfepregs  35327  dfon2lem3  36024  bj-ccinftydisj  37586  nninfnub  38131  ispridl2  38418  rp-isfinite6  43975  fnresfnco  47516