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  13896  rrxcph  25317  volun  25471  umgrislfupgr  29099  usgrislfuspgr  29163  wlkp1lem8  29655  dfpth2  29705  elwwlks2s3  29927  eupthp1  30191  cnvbraval  32085  brab2d  32583  ballotlemfp1  34500  finixpnum  37644  fin2so  37646  matunitlindflem1  37655  oeord2com  43343  clsf2  44158  ellimcabssub0  45656  sge0iunmpt  46455  icceuelpartlem  47465  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  grtrif1o  47972  brab2dd  48858