Theorem sylbb 219

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 216	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	sylbi 217	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  bitri  275  elabgtOLDOLD  3629  ssdifim  4223  ralf0  4464  disjxiun  5088  wefrc  5610  frsn  5704  ssrel  5723  funiun  7080  funopsn  7081  ssfi  9082  enfii  9095  nneneq  9115  fissuni  9241  inf3lem2  9519  rankvalb  9687  djur  9809  xrrebnd  13064  xaddf  13120  elfznelfzob  13671  fsuppmapnn0ub  13899  hashinfxadd  14289  hashfun  14341  fz1f1o  15614  dvdszzq  16629  clatl  18411  sgrp2nmndlem5  18834  mat1dimelbas  22384  cfinfil  23806  dyadmax  25524  ausgrusgri  29144  nbupgrres  29340  usgredgsscusgredg  29436  1egrvtxdg0  29488  wlkp1lem7  29654  isch3  31216  nmopun  31989  2ndresdju  32626  cycpm2tr  33083  elrgspnlem1  33204  elrgspnlem2  33205  fldextrspunlsplem  33681  esumnul  34056  dya2iocnrect  34289  bnj849  34932  bnj1279  35025  cusgr3cyclex  35168  in-ax8  36257  bj-0int  37134  onsucuni3  37400  wl-nfeqfb  37569  poimirlem27  37686  sticksstones20  42198  fimgmcyclem  42565  sucomisnotcard  43576  iunrelexp0  43734  frege129d  43795  clsk3nimkb  44072  gneispace  44166  eliuniin  45135  eliuniin2  45156  stoweidlem48  46085  fourierdlem42  46186  fourierdlem80  46223  eubrdm  47066  oddprmALTV  47717  grtriproplem  47969  grtrif1o  47972  pgnbgreunbgr  48155  alimp-no-surprise  49812