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  5512  fsuppmapnn0fiubex  14115  matunitlindflem1  22974  rrxcph  25693  volun  25846  umgrislfupgr  29683  usgrislfuspgr  29750  wlkp1lem8  30241  dfpth2  30296  elwwlks2s3  30522  eupthp1  30799  cnvbraval  32694  ballotlemfp1  35107  finixpnum  38496  fin2so  38498  oeord2com  44271  clsf2  45085  ellimcabssub0  46573  sge0iunmpt  47372  icceuelpartlem  48461  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  grtrif1o  48984  brab2dd  49882