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  13917  rrxcph  25308  volun  25462  umgrislfupgr  29086  usgrislfuspgr  29150  wlkp1lem8  29642  dfpth2  29692  elwwlks2s3  29914  eupthp1  30178  cnvbraval  32072  brab2d  32568  ballotlemfp1  34459  finixpnum  37584  fin2so  37586  matunitlindflem1  37595  oeord2com  43284  clsf2  44099  ellimcabssub0  45599  sge0iunmpt  46400  icceuelpartlem  47420  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  grtrif1o  47927  brab2dd  48813