Theorem sylbb 222

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 219	. 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:  bitri  278  ssdifim  4228  disjxiun  5102  wefrc  5646  frsn  5740  ssrel  5760  funiun  7133  funopsn  7134  funopsnOLD  7135  ssfi  9145  enfii  9158  nneneq  9178  fissuni  9302  inf3lem2  9586  rankvalb  9757  djur  9893  xrrebnd  13185  xaddf  13241  elfznelfzob  13794  fsuppmapnn0ub  14022  hashinfxadd  14412  hashfun  14464  fz1f1o  15751  dvdszzq  16770  clatl  18554  sgrp2nmndlem5  18981  mat1dimelbas  22589  cfinfil  24011  dyadmax  25718  ausgrusgri  29427  nbupgrres  29623  usgredgsscusgredg  29718  1egrvtxdg0  29770  wlkp1lem7  29936  isch3  31502  nmopun  32275  2ndresdju  32906  cycpm2tr  33352  elrgspnlem1  33475  elrgspnlem2  33476  fldextrspunlsplem  33980  esumnul  34355  dya2iocnrect  34588  bnj849  35230  bnj1279  35323  cusgr3cyclex  35499  in-ax8  36597  regsfromunir1  36913  bj-0int  37603  onsucuni3  37873  wl-nfeqfb  38051  poimirlem27  38158  sticksstones20  42795  fimgmcyclem  43163  sucomisnotcard  44132  iunrelexp0  44290  frege129d  44351  clsk3nimkb  44628  gneispace  44722  eliuniin  45675  eliuniin2  45696  stoweidlem48  46620  fourierdlem42  46721  fourierdlem80  46758  eubrdm  47628  oddprmALTV  48307  grtriproplem  48559  grtrif1o  48562  pgnbgreunbgr  48745  alimp-no-surprise  50410