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  4218  disjxiun  5099  wefrc  5644  frsn  5738  ssrel  5758  funiun  7150  funopsn  7151  funopsnOLD  7152  ssfi  9191  enfii  9204  nneneq  9224  fissuni  9349  inf3lem2  9633  rankvalb  9808  hffi  9912  djur  10003  xrrebnd  13301  xaddf  13357  elfznelfzob  13912  fsuppmapnn0ub  14141  hashinfxadd  14532  hashfun  14585  fz1f1o  15881  dvdszzq  16902  clatl  18687  sgrp2nmndlem5  19133  mat1dimelbas  22791  cfinfil  24217  dyadmax  25924  ausgrusgri  29754  nbupgrres  29950  usgredgsscusgredg  30045  1egrvtxdg0  30097  wlkp1lem7  30263  isch3  31848  nmopun  32621  2ndresdju  33290  acunirnmpt2  33301  cycpm2tr  33726  elrgspnlem1  33849  elrgspnlem2  33850  fldextrspunlsplem  34351  esumnul  34726  dya2iocnrect  34959  bnj849  35601  bnj1279  35694  rankscott  35806  cusgr3cyclex  35987  in-ax8  37105  regsfromunir1  37420  bj-vn0ALT  38079  bj-0int  38114  onsucuni3  38383  wl-nfeqfb  38561  poimirlem27  38658  sticksstones20  43309  fimgmcyclem  43690  sucomisnotcard  44638  iunrelexp0  44795  frege129d  44856  clsk3nimkb  45133  gneispace  45227  eliuniin  46207  eliuniin2  46228  stoweidlem48  47151  fourierdlem42  47252  fourierdlem80  47289  eubrdm  48199  oddprmALTV  48878  grtriproplem  49130  grtrif1o  49133  pgnbgreunbgr  49316  alimp-no-surprise  51045