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  13964  rrxcph  25299  volun  25453  umgrislfupgr  29057  usgrislfuspgr  29121  wlkp1lem8  29615  dfpth2  29666  elwwlks2s3  29888  eupthp1  30152  cnvbraval  32046  brab2d  32542  ballotlemfp1  34490  finixpnum  37606  fin2so  37608  matunitlindflem1  37617  oeord2com  43307  clsf2  44122  ellimcabssub0  45622  sge0iunmpt  46423  icceuelpartlem  47440  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  grtrif1o  47945  brab2dd  48820