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  13993  rrxcph  25364  volun  25518  umgrislfupgr  29008  usgrislfuspgr  29072  wlkp1lem8  29566  elwwlks2s3  29834  eupthp1  30098  cnvbraval  31992  brab2d  32476  ballotlemfp1  34242  finixpnum  37209  fin2so  37211  matunitlindflem1  37220  oeord2com  42882  clsf2  43698  ellimcabssub0  45143  sge0iunmpt  45944  icceuelpartlem  46912  nnsum4primesodd  47273  nnsum4primesoddALTV  47274