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  14033  rrxcph  25426  volun  25580  umgrislfupgr  29140  usgrislfuspgr  29204  wlkp1lem8  29698  dfpth2  29749  elwwlks2s3  29971  eupthp1  30235  cnvbraval  32129  brab2d  32619  ballotlemfp1  34494  finixpnum  37612  fin2so  37614  matunitlindflem1  37623  oeord2com  43324  clsf2  44139  ellimcabssub0  45632  sge0iunmpt  46433  icceuelpartlem  47422  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  grtrif1o  47909  brab2dd  48741