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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bitri  278  ssdifim  4221  disjxiun  5103  wefrc  5649  frsn  5744  ssrel  5764  funiun  7174  funopsn  7175  funopsnOLD  7176  ssfi  9216  enfii  9229  nneneq  9249  fissuni  9374  inf3lem2  9657  rankvalb  9832  hffi  9936  djur  10027  xrrebnd  13325  xaddf  13381  elfznelfzob  13936  fsuppmapnn0ub  14165  hashinfxadd  14556  hashfun  14609  fz1f1o  15905  dvdszzq  16926  clatl  18711  sgrp2nmndlem5  19157  mat1dimelbas  22816  cfinfil  24242  dyadmax  25949  ausgrusgri  29779  nbupgrres  29975  usgredgsscusgredg  30070  1egrvtxdg0  30122  wlkp1lem7  30288  isch3  31873  nmopun  32646  2ndresdju  33315  acunirnmpt2  33326  cycpm2tr  33750  elrgspnlem1  33873  elrgspnlem2  33874  fldextrspunlsplem  34375  esumnul  34750  dya2iocnrect  34983  bnj849  35625  bnj1279  35718  rankscott  35838  cusgr3cyclex  36068  in-ax8  37191  regsfromunir1  37506  bj-vn0ALT  38178  bj-0int  38213  onsucuni3  38482  wl-nfeqfb  38660  poimirlem27  38757  sticksstones20  43408  fimgmcyclem  43790  sucomisnotcard  44737  iunrelexp0  44894  frege129d  44955  clsk3nimkb  45232  gneispace  45326  eliuniin  46319  eliuniin2  46340  stoweidlem48  47263  fourierdlem42  47364  fourierdlem80  47401  eubrdm  48311  oddprmALTV  48990  grtriproplem  49242  grtrif1o  49245  pgnbgreunbgr  49428  alimp-no-surprise  51157