Theorem sylbb1 236

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 227	. 2 ⊢ (𝜓 → 𝜑)
3		sylbb1.2	. 2 ⊢ (𝜑 ↔ 𝜒)
4	2, 3	sylib 217	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  fsuppmapnn0fiubex  13693  rrxcph  24537  volun  24690  umgrislfupgr  27474  usgrislfuspgr  27535  wlkp1lem8  28028  elwwlks2s3  28295  eupthp1  28559  cnvbraval  30451  ballotlemfp1  32437  finixpnum  35741  fin2so  35743  matunitlindflem1  35752  clsf2  41689  ellimcabssub0  43112  sge0iunmpt  43910  icceuelpartlem  44839  nnsum4primesodd  45200  nnsum4primesoddALTV  45201