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  13927  rrxcph  25360  volun  25514  umgrislfupgr  29208  usgrislfuspgr  29272  wlkp1lem8  29764  dfpth2  29814  elwwlks2s3  30036  eupthp1  30303  cnvbraval  32197  brab2d  32694  ballotlemfp1  34669  finixpnum  37850  fin2so  37852  matunitlindflem1  37861  oeord2com  43662  clsf2  44476  ellimcabssub0  45971  sge0iunmpt  46770  icceuelpartlem  47789  nnsum4primesodd  48150  nnsum4primesoddALTV  48151  grtrif1o  48296  brab2dd  49181