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  5516  imadifssrn  6214  fsuppmapnn0fiubex  14162  matunitlindflem1  23024  rrxcph  25743  volun  25896  umgrislfupgr  29731  usgrislfuspgr  29798  wlkp1lem8  30289  dfpth2  30344  elwwlks2s3  30570  eupthp1  30847  cnvbraval  32742  ballotlemfp1  35194  finixpnum  38720  fin2so  38722  frlmnzcoordex  43845  oeord2com  44505  clsf2  45318  ellimcabssub0  46834  sge0iunmpt  47633  icceuelpartlem  48722  nnsum4primesodd  49099  nnsum4primesoddALTV  49100  grtrif1o  49245  brab2dd  50144