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  14030  rrxcph  25440  volun  25594  umgrislfupgr  29155  usgrislfuspgr  29219  wlkp1lem8  29713  elwwlks2s3  29981  eupthp1  30245  cnvbraval  32139  brab2d  32627  ballotlemfp1  34473  finixpnum  37592  fin2so  37594  matunitlindflem1  37603  oeord2com  43301  clsf2  44116  ellimcabssub0  45573  sge0iunmpt  46374  icceuelpartlem  47360  nnsum4primesodd  47721  nnsum4primesoddALTV  47722  grtrif1o  47847