Theorem sylbb 221

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bitri  277  unitreslOLD  874  ssdifim  4238  disjxiun  5055  pocl  5475  wefrc  5543  frsn  5633  ssrel  5651  funiun  6903  funopsn  6904  fissuni  8823  inf3lem2  9086  rankvalb  9220  djur  9342  xrrebnd  12555  xaddf  12611  elfznelfzob  13137  fsuppmapnn0ub  13357  hashinfxadd  13740  hashfun  13792  fz1f1o  15061  clatl  17720  sgrp2nmndlem5  18088  mat1dimelbas  21074  cfinfil  22495  dyadmax  24193  ausgrusgri  26947  nbupgrres  27140  usgredgsscusgredg  27235  1egrvtxdg0  27287  wlkp1lem7  27455  wwlksnfiOLD  27679  isch3  29012  nmopun  29785  dvdszzq  30525  cycpm2tr  30756  esumnul  31302  dya2iocnrect  31534  bnj849  32192  bnj1279  32285  cusgr3cyclex  32378  bj-0int  34387  onsucuni3  34642  wl-nfeqfb  34770  poimirlem27  34913  iunrelexp0  40040  frege129d  40101  clsk3nimkb  40383  gneispace  40477  eliuniin  41358  eliuniin2  41379  stoweidlem48  42327  fourierdlem42  42428  fourierdlem80  42465  eubrdm  43265  oddprmALTV  43846  alimp-no-surprise  44876