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  13901  rrxcph  25320  volun  25474  umgrislfupgr  29103  usgrislfuspgr  29167  wlkp1lem8  29659  dfpth2  29709  elwwlks2s3  29931  eupthp1  30198  cnvbraval  32092  brab2d  32590  ballotlemfp1  34526  finixpnum  37665  fin2so  37667  matunitlindflem1  37676  oeord2com  43428  clsf2  44243  ellimcabssub0  45741  sge0iunmpt  46540  icceuelpartlem  47559  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  grtrif1o  48066  brab2dd  48952