Theorem sylbb1 240

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  brab2d  5524  fsuppmapnn0fiubex  14030  rrxcph  25532  volun  25685  umgrislfupgr  29451  usgrislfuspgr  29515  wlkp1lem8  30006  dfpth2  30056  elwwlks2s3  30278  eupthp1  30545  cnvbraval  32440  ballotlemfp1  34860  finixpnum  38234  fin2so  38236  matunitlindflem1  38245  oeord2com  44018  clsf2  44832  ellimcabssub0  46313  sge0iunmpt  47112  icceuelpartlem  48161  nnsum4primesodd  48538  nnsum4primesoddALTV  48539  grtrif1o  48684  brab2dd  49583