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  13945  rrxcph  25369  volun  25522  umgrislfupgr  29206  usgrislfuspgr  29270  wlkp1lem8  29762  dfpth2  29812  elwwlks2s3  30034  eupthp1  30301  cnvbraval  32196  brab2d  32693  ballotlemfp1  34652  finixpnum  37940  fin2so  37942  matunitlindflem1  37951  oeord2com  43757  clsf2  44571  ellimcabssub0  46065  sge0iunmpt  46864  icceuelpartlem  47907  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  grtrif1o  48430  brab2dd  49315