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  13943  rrxcph  25347  volun  25500  umgrislfupgr  29180  usgrislfuspgr  29244  wlkp1lem8  29735  dfpth2  29785  elwwlks2s3  30007  eupthp1  30274  cnvbraval  32169  brab2d  32666  ballotlemfp1  34624  finixpnum  37914  fin2so  37916  matunitlindflem1  37925  oeord2com  43727  clsf2  44541  ellimcabssub0  46035  sge0iunmpt  46834  icceuelpartlem  47883  nnsum4primesodd  48260  nnsum4primesoddALTV  48261  grtrif1o  48406  brab2dd  49291