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  4222  disjxiun  5104  wefrc  5653  frsn  5747  ssrel  5767  funiun  7147  funopsn  7148  funopsnOLD  7149  ssfi  9171  enfii  9184  nneneq  9204  fissuni  9328  inf3lem2  9612  rankvalb  9783  djur  9928  xrrebnd  13224  xaddf  13280  elfznelfzob  13834  fsuppmapnn0ub  14063  hashinfxadd  14453  hashfun  14506  fz1f1o  15800  dvdszzq  16818  clatl  18602  sgrp2nmndlem5  19047  mat1dimelbas  22699  cfinfil  24125  dyadmax  25832  ausgrusgri  29636  nbupgrres  29832  usgredgsscusgredg  29927  1egrvtxdg0  29979  wlkp1lem7  30145  isch3  31730  nmopun  32503  2ndresdju  33130  cycpm2tr  33567  elrgspnlem1  33690  elrgspnlem2  33691  fldextrspunlsplem  34191  esumnul  34566  dya2iocnrect  34800  bnj849  35442  bnj1279  35535  rankscott  35643  cusgr3cyclex  35733  in-ax8  36852  regsfromunir1  37167  bj-vn0ALT  37824  bj-0int  37859  onsucuni3  38129  wl-nfeqfb  38307  poimirlem27  38404  sticksstones20  43040  fimgmcyclem  43423  sucomisnotcard  44392  iunrelexp0  44550  frege129d  44611  clsk3nimkb  44888  gneispace  44982  eliuniin  45939  eliuniin2  45960  stoweidlem48  46884  fourierdlem42  46985  fourierdlem80  47022  eubrdm  47932  oddprmALTV  48611  grtriproplem  48863  grtrif1o  48866  pgnbgreunbgr  49049  alimp-no-surprise  50718