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  13957  rrxcph  24909  volun  25062  umgrislfupgr  28414  usgrislfuspgr  28475  wlkp1lem8  28968  elwwlks2s3  29236  eupthp1  29500  cnvbraval  31394  ballotlemfp1  33521  finixpnum  36521  fin2so  36523  matunitlindflem1  36532  oeord2com  42109  clsf2  42925  ellimcabssub0  44381  sge0iunmpt  45182  icceuelpartlem  46151  nnsum4primesodd  46512  nnsum4primesoddALTV  46513