Theorem sylbb1 237

Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.)

Hypotheses

Ref	Expression
sylbb1.1	⊢ (𝜑 ↔ 𝜓)
sylbb1.2	⊢ (𝜑 ↔ 𝜒)

Assertion

Ref	Expression
sylbb1	⊢ (𝜓 → 𝜒)

Proof of Theorem sylbb1

Step	Hyp	Ref	Expression
1		sylbb1.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpri 228	. 2 ⊢ (𝜓 → 𝜑)
3		sylbb1.2	. 2 ⊢ (𝜑 ↔ 𝜒)
4	2, 3	sylib 218	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:  fsuppmapnn0fiubex  14043  rrxcph  25445  volun  25599  umgrislfupgr  29158  usgrislfuspgr  29222  wlkp1lem8  29716  elwwlks2s3  29984  eupthp1  30248  cnvbraval  32142  brab2d  32629  ballotlemfp1  34456  finixpnum  37565  fin2so  37567  matunitlindflem1  37576  oeord2com  43273  clsf2  44088  ellimcabssub0  45538  sge0iunmpt  46339  icceuelpartlem  47309  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  grtrif1o  47793