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  5511  imadifssrn  6201  fsuppmapnn0fiubex  14138  matunitlindflem1  22999  rrxcph  25718  volun  25871  umgrislfupgr  29706  usgrislfuspgr  29773  wlkp1lem8  30264  dfpth2  30319  elwwlks2s3  30545  eupthp1  30822  cnvbraval  32717  ballotlemfp1  35170  finixpnum  38621  fin2so  38623  frlmnzcoordex  43745  oeord2com  44406  clsf2  45219  ellimcabssub0  46722  sge0iunmpt  47521  icceuelpartlem  48610  nnsum4primesodd  48987  nnsum4primesoddALTV  48988  grtrif1o  49133  brab2dd  50032