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  34702  bnj849  35344  bnj1279  35437  rankscott  35545  cusgr3cyclex  35648  in-ax8  36776  regsfromunir1  37091  bj-vn0ALT  37748  bj-0int  37783  onsucuni3  38053  wl-nfeqfb  38231  poimirlem27  38338  sticksstones20  42973  fimgmcyclem  43341  sucomisnotcard  44310  iunrelexp0  44468  frege129d  44529  clsk3nimkb  44806  gneispace  44900  eliuniin  45857  eliuniin2  45878  stoweidlem48  46802  fourierdlem42  46903  fourierdlem80  46940  eubrdm  47813  oddprmALTV  48492  grtriproplem  48744  grtrif1o  48747  pgnbgreunbgr  48930  alimp-no-surprise  50599