Theorem sylbb 218

Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.)

Hypotheses

Ref	Expression
sylbb.1	⊢ (𝜑 ↔ 𝜓)
sylbb.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
sylbb	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbb

Step	Hyp	Ref	Expression
1		sylbb.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		sylbb.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	biimpi 215	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	sylbi 216	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitri  275  unitreslOLD  877  elabgt  3663  ssdifim  4263  ralf0  4514  disjxiun  5146  poclOLD  5597  wefrc  5671  frsn  5764  ssrel  5783  ssrelOLD  5784  funiun  7145  funopsn  7146  ssfi  9173  enfii  9189  nneneq  9209  fissuni  9357  inf3lem2  9624  rankvalb  9792  djur  9914  xrrebnd  13147  xaddf  13203  elfznelfzob  13738  fsuppmapnn0ub  13960  hashinfxadd  14345  hashfun  14397  fz1f1o  15656  clatl  18461  sgrp2nmndlem5  18810  mat1dimelbas  21973  cfinfil  23397  dyadmax  25115  ausgrusgri  28428  nbupgrres  28621  usgredgsscusgredg  28716  1egrvtxdg0  28768  wlkp1lem7  28936  isch3  30494  nmopun  31267  2ndresdju  31874  dvdszzq  32021  cycpm2tr  32278  esumnul  33046  dya2iocnrect  33280  bnj849  33936  bnj1279  34029  cusgr3cyclex  34127  bj-0int  35982  onsucuni3  36248  wl-nfeqfb  36405  poimirlem27  36515  sticksstones20  40982  sucomisnotcard  42295  iunrelexp0  42453  frege129d  42514  clsk3nimkb  42791  gneispace  42885  eliuniin  43788  eliuniin2  43809  stoweidlem48  44764  fourierdlem42  44865  fourierdlem80  44902  eubrdm  45746  oddprmALTV  46355  alimp-no-surprise  47828