Theorem sylbb1 226

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  moeq  3349  fsuppmapnn0fiubex  12654  rrxcph  22988  umgrislfupgr  25789  cnvbraval  28353  ballotlemfp1  29880  finixpnum  32564  fin2so  32566  matunitlindflem1  32575  clsf2  37444  ellimcabssub0  38684  sge0iunmpt  39311  icceuelpartlem  39973  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  usgrislfuspgr  40414  1wlkp1lem8  40889  elwwlks2s3  41169  eupthp1  41384