Theorem sylbb1 236

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 227	. 2 ⊢ (𝜓 → 𝜑)
3		sylbb1.2	. 2 ⊢ (𝜑 ↔ 𝜒)
4	2, 3	sylib 217	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  fsuppmapnn0fiubex  13710  rrxcph  24554  volun  24707  umgrislfupgr  27491  usgrislfuspgr  27552  wlkp1lem8  28045  elwwlks2s3  28312  eupthp1  28576  cnvbraval  30468  ballotlemfp1  32454  finixpnum  35758  fin2so  35760  matunitlindflem1  35769  clsf2  41706  ellimcabssub0  43129  sge0iunmpt  43927  icceuelpartlem  44856  nnsum4primesodd  45217  nnsum4primesoddALTV  45218