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  274  unitreslOLD  876  elabgt  3662  ssdifim  4262  ralf0  4513  disjxiun  5145  poclOLD  5596  wefrc  5670  frsn  5763  ssrel  5782  ssrelOLD  5783  funiun  7144  funopsn  7145  ssfi  9172  enfii  9188  nneneq  9208  fissuni  9356  inf3lem2  9623  rankvalb  9791  djur  9913  xrrebnd  13146  xaddf  13202  elfznelfzob  13737  fsuppmapnn0ub  13959  hashinfxadd  14344  hashfun  14396  fz1f1o  15655  clatl  18460  sgrp2nmndlem5  18809  mat1dimelbas  21972  cfinfil  23396  dyadmax  25114  ausgrusgri  28425  nbupgrres  28618  usgredgsscusgredg  28713  1egrvtxdg0  28765  wlkp1lem7  28933  isch3  30489  nmopun  31262  2ndresdju  31869  dvdszzq  32016  cycpm2tr  32273  esumnul  33041  dya2iocnrect  33275  bnj849  33931  bnj1279  34024  cusgr3cyclex  34122  bj-0int  35977  onsucuni3  36243  wl-nfeqfb  36400  poimirlem27  36510  sticksstones20  40977  sucomisnotcard  42285  iunrelexp0  42443  frege129d  42504  clsk3nimkb  42781  gneispace  42875  eliuniin  43778  eliuniin2  43799  stoweidlem48  44754  fourierdlem42  44855  fourierdlem80  44892  eubrdm  45736  oddprmALTV  46345  alimp-no-surprise  47818