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  3382  fsuppmapnn0fiubex  12792  rrxcph  23180  umgrislfupgr  26018  usgrislfuspgr  26079  wlkp1lem8  26577  elwwlks2s3  26859  eupthp1  27076  cnvbraval  28969  ballotlemfp1  30553  finixpnum  33394  fin2so  33396  matunitlindflem1  33405  clsf2  38424  ellimcabssub0  39849  sge0iunmpt  40635  icceuelpartlem  41371  nnsum4primesodd  41684  nnsum4primesoddALTV  41685