Theorem sylbb1 239

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  fsuppmapnn0fiubex  14002  rrxcph  25434  volun  25587  umgrislfupgr  29270  usgrislfuspgr  29334  wlkp1lem8  29825  dfpth2  29875  elwwlks2s3  30097  eupthp1  30364  cnvbraval  32259  brab2d  32757  ballotlemfp1  34750  finixpnum  38068  fin2so  38070  matunitlindflem1  38079  oeord2com  43852  clsf2  44666  ellimcabssub0  46157  sge0iunmpt  46956  icceuelpartlem  48005  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  grtrif1o  48528  brab2dd  49413