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  13954  rrxcph  25359  volun  25512  umgrislfupgr  29192  usgrislfuspgr  29256  wlkp1lem8  29747  dfpth2  29797  elwwlks2s3  30019  eupthp1  30286  cnvbraval  32181  brab2d  32678  ballotlemfp1  34636  finixpnum  37926  fin2so  37928  matunitlindflem1  37937  oeord2com  43739  clsf2  44553  ellimcabssub0  46047  sge0iunmpt  46846  icceuelpartlem  47895  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  grtrif1o  48418  brab2dd  49303