Theorem sylbb1 239

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  fsuppmapnn0fiubex  13361  rrxcph  23995  volun  24146  umgrislfupgr  26908  usgrislfuspgr  26969  wlkp1lem8  27462  elwwlks2s3  27730  eupthp1  27995  cnvbraval  29887  ballotlemfp1  31749  finixpnum  34892  fin2so  34894  matunitlindflem1  34903  clsf2  40496  ellimcabssub0  41918  sge0iunmpt  42720  icceuelpartlem  43615  nnsum4primesodd  43981  nnsum4primesoddALTV  43982