Theorem sylbb1 240

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  fsuppmapnn0fiubex  13565  rrxcph  24289  volun  24442  umgrislfupgr  27214  usgrislfuspgr  27275  wlkp1lem8  27768  elwwlks2s3  28035  eupthp1  28299  cnvbraval  30191  ballotlemfp1  32170  finixpnum  35499  fin2so  35501  matunitlindflem1  35510  clsf2  41413  ellimcabssub0  42833  sge0iunmpt  43631  icceuelpartlem  44560  nnsum4primesodd  44921  nnsum4primesoddALTV  44922