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  14010  rrxcph  25344  volun  25498  umgrislfupgr  29102  usgrislfuspgr  29166  wlkp1lem8  29660  dfpth2  29711  elwwlks2s3  29933  eupthp1  30197  cnvbraval  32091  brab2d  32587  ballotlemfp1  34524  finixpnum  37629  fin2so  37631  matunitlindflem1  37640  oeord2com  43335  clsf2  44150  ellimcabssub0  45646  sge0iunmpt  46447  icceuelpartlem  47449  nnsum4primesodd  47810  nnsum4primesoddALTV  47811  grtrif1o  47954  brab2dd  48806