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 ⊢ (𝜓 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  brab2d  5520  fsuppmapnn0fiubex  14060  matunitlindflem1  22907  rrxcph  25626  volun  25779  umgrislfupgr  29588  usgrislfuspgr  29655  wlkp1lem8  30146  dfpth2  30201  elwwlks2s3  30427  eupthp1  30704  cnvbraval  32599  ballotlemfp1  35011  finixpnum  38367  fin2so  38369  oeord2com  44160  clsf2  44974  ellimcabssub0  46455  sge0iunmpt  47254  icceuelpartlem  48343  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  grtrif1o  48866  brab2dd  49764