Theorem sylbb 218

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitri  274  unitreslOLD  875  elabgt  3604  ssdifim  4197  ralf0  4445  disjxiun  5072  poclOLD  5512  wefrc  5584  frsn  5675  ssrel  5694  ssrelOLD  5695  funiun  7028  funopsn  7029  ssfi  8965  enfii  8981  nneneq  9001  fissuni  9133  inf3lem2  9396  rankvalb  9564  djur  9686  xrrebnd  12911  xaddf  12967  elfznelfzob  13502  fsuppmapnn0ub  13724  hashinfxadd  14109  hashfun  14161  fz1f1o  15431  clatl  18235  sgrp2nmndlem5  18577  mat1dimelbas  21629  cfinfil  23053  dyadmax  24771  ausgrusgri  27547  nbupgrres  27740  usgredgsscusgredg  27835  1egrvtxdg0  27887  wlkp1lem7  28056  isch3  29612  nmopun  30385  2ndresdju  30995  dvdszzq  31138  cycpm2tr  31395  esumnul  32025  dya2iocnrect  32257  bnj849  32914  bnj1279  33007  cusgr3cyclex  33107  bj-0int  35281  onsucuni3  35547  wl-nfeqfb  35704  poimirlem27  35813  sticksstones20  40129  sucomisnotcard  41158  iunrelexp0  41317  frege129d  41378  clsk3nimkb  41657  gneispace  41751  eliuniin  42656  eliuniin2  42676  stoweidlem48  43596  fourierdlem42  43697  fourierdlem80  43734  eubrdm  44541  oddprmALTV  45150  alimp-no-surprise  46496