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  13915  rrxcph  25348  volun  25502  umgrislfupgr  29196  usgrislfuspgr  29260  wlkp1lem8  29752  dfpth2  29802  elwwlks2s3  30024  eupthp1  30291  cnvbraval  32185  brab2d  32683  ballotlemfp1  34649  finixpnum  37802  fin2so  37804  matunitlindflem1  37813  oeord2com  43549  clsf2  44363  ellimcabssub0  45859  sge0iunmpt  46658  icceuelpartlem  47677  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  grtrif1o  48184  brab2dd  49069