Theorem sylbb1 227

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  moeq  3515  fsuppmapnn0fiubex  12978  rrxcph  23372  umgrislfupgr  26209  usgrislfuspgr  26270  wlkp1lem8  26779  elwwlks2s3  27063  eupthp1  27360  cnvbraval  29270  ballotlemfp1  30854  finixpnum  33699  fin2so  33701  matunitlindflem1  33710  clsf2  38918  ellimcabssub0  40344  sge0iunmpt  41130  icceuelpartlem  41873  nnsum4primesodd  42186  nnsum4primesoddALTV  42187