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  5527  fsuppmapnn0fiubex  14048  rrxcph  25588  volun  25741  umgrislfupgr  29510  usgrislfuspgr  29574  wlkp1lem8  30065  dfpth2  30115  elwwlks2s3  30337  eupthp1  30604  cnvbraval  32499  ballotlemfp1  34914  finixpnum  38297  fin2so  38299  matunitlindflem1  38308  oeord2com  44079  clsf2  44893  ellimcabssub0  46374  sge0iunmpt  47173  icceuelpartlem  48225  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  grtrif1o  48748  brab2dd  49647