Theorem sylbb 209

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  bitri  264  ssdifim  3895  disjxiun  4681  trint  4801  pocl  5071  wefrc  5137  frsn  5223  ssrel  5241  funiun  6452  funopsn  6453  fissuni  8312  inf3lem2  8564  rankvalb  8698  xrrebnd  12037  xaddf  12093  elfznelfzob  12614  fsuppmapnn0ub  12835  hashinfxadd  13212  hashfun  13262  fz1f1o  14485  clatl  17163  sgrp2nmndlem5  17463  mat1dimelbas  20325  cfinfil  21744  dyadmax  23412  ausgrusgri  26108  nbupgrres  26310  usgredgsscusgredg  26411  1egrvtxdg0  26463  wlkp1lem7  26632  wwlksnfi  26869  isch3  28226  nmopun  29001  esumnul  30238  dya2iocnrect  30471  bnj849  31121  bnj1279  31212  bj-0int  33180  onsucuni3  33345  wl-nfeqfb  33453  poimirlem27  33566  unitresl  34014  iunrelexp0  38311  frege129d  38372  clsk3nimkb  38655  gneispace  38749  eliuniin  39593  eliuniin2  39617  stoweidlem48  40583  fourierdlem42  40684  fourierdlem80  40721  oddprmALTV  41923  alimp-no-surprise  42855