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  13758  rrxcph  24601  volun  24754  umgrislfupgr  27538  usgrislfuspgr  27599  wlkp1lem8  28093  elwwlks2s3  28361  eupthp1  28625  cnvbraval  30517  ballotlemfp1  32503  finixpnum  35806  fin2so  35808  matunitlindflem1  35817  clsf2  41774  ellimcabssub0  43207  sge0iunmpt  44006  icceuelpartlem  44945  nnsum4primesodd  45306  nnsum4primesoddALTV  45307