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:  brab2d  5513  fsuppmapnn0fiubex  14019  rrxcph  25512  volun  25665  umgrislfupgr  29382  usgrislfuspgr  29446  wlkp1lem8  29937  dfpth2  29987  elwwlks2s3  30209  eupthp1  30476  cnvbraval  32371  ballotlemfp1  34799  finixpnum  38116  fin2so  38118  matunitlindflem1  38127  oeord2com  43900  clsf2  44714  ellimcabssub0  46191  sge0iunmpt  46990  icceuelpartlem  48039  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  grtrif1o  48562  brab2dd  49457