Theorem sylbb1 238

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  fsuppmapnn0fiubex  13952  rrxcph  25384  volun  25537  umgrislfupgr  29217  usgrislfuspgr  29281  wlkp1lem8  29772  dfpth2  29822  elwwlks2s3  30044  eupthp1  30311  cnvbraval  32206  brab2d  32704  ballotlemfp1  34683  finixpnum  37979  fin2so  37981  matunitlindflem1  37990  oeord2com  43763  clsf2  44577  ellimcabssub0  46069  sge0iunmpt  46868  icceuelpartlem  47917  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  grtrif1o  48440  brab2dd  49325