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  13999  rrxcph  25329  volun  25483  umgrislfupgr  29034  usgrislfuspgr  29098  wlkp1lem8  29592  dfpth2  29643  elwwlks2s3  29865  eupthp1  30129  cnvbraval  32023  brab2d  32520  ballotlemfp1  34432  finixpnum  37550  fin2so  37552  matunitlindflem1  37561  oeord2com  43260  clsf2  44075  ellimcabssub0  45576  sge0iunmpt  46377  icceuelpartlem  47367  nnsum4primesodd  47728  nnsum4primesoddALTV  47729  grtrif1o  47854  brab2dd  48687