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  4229  disjxiun  5111  wefrc  5660  frsn  5754  ssrel  5774  funiun  7150  funopsn  7151  funopsnOLD  7152  ssfi  9167  enfii  9180  nneneq  9200  fissuni  9324  inf3lem2  9608  rankvalb  9779  djur  9924  xrrebnd  13212  xaddf  13268  elfznelfzob  13822  fsuppmapnn0ub  14051  hashinfxadd  14441  hashfun  14494  fz1f1o  15787  dvdszzq  16805  clatl  18589  sgrp2nmndlem5  19022  mat1dimelbas  22665  cfinfil  24087  dyadmax  25794  ausgrusgri  29555  nbupgrres  29751  usgredgsscusgredg  29846  1egrvtxdg0  29898  wlkp1lem7  30064  isch3  31630  nmopun  32403  2ndresdju  33031  cycpm2tr  33470  elrgspnlem1  33593  elrgspnlem2  33594  fldextrspunlsplem  34094  esumnul  34469  dya2iocnrect  34703  bnj849  35345  bnj1279  35438  rankscott  35546  cusgr3cyclex  35649  in-ax8  36777  regsfromunir1  37092  bj-vn0ALT  37749  bj-0int  37784  onsucuni3  38054  wl-nfeqfb  38232  poimirlem27  38339  sticksstones20  42974  fimgmcyclem  43342  sucomisnotcard  44311  iunrelexp0  44469  frege129d  44530  clsk3nimkb  44807  gneispace  44901  eliuniin  45858  eliuniin2  45879  stoweidlem48  46803  fourierdlem42  46904  fourierdlem80  46941  eubrdm  47814  oddprmALTV  48493  grtriproplem  48745  grtrif1o  48748  pgnbgreunbgr  48931  alimp-no-surprise  50600