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  13957  rrxcph  25292  volun  25446  umgrislfupgr  29050  usgrislfuspgr  29114  wlkp1lem8  29608  dfpth2  29659  elwwlks2s3  29881  eupthp1  30145  cnvbraval  32039  brab2d  32535  ballotlemfp1  34483  finixpnum  37599  fin2so  37601  matunitlindflem1  37610  oeord2com  43300  clsf2  44115  ellimcabssub0  45615  sge0iunmpt  46416  icceuelpartlem  47436  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  grtrif1o  47941  brab2dd  48816