Theorem sylbb2 238

Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.)

Hypotheses

Ref	Expression
sylbb2.1	⊢ (𝜑 ↔ 𝜓)
sylbb2.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
sylbb2	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbb2

Step	Hyp	Ref	Expression
1		sylbb2.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		sylbb2.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	biimpri 228	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	sylbi 217	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  rexprg  4654  ftpg  7101  frrlem13  8240  brinxper  8664  sdom0  9037  funsnfsupp  9295  sucprcreg  9509  fin23lem40  10261  ffz0iswrd  14464  s4f1o  14841  fsumsplitsnun  15678  lcmcllem  16523  catcone0  17610  lidldvgen  21289  mat1dimbas  22416  pmatcollpw3fi  22729  nbgrssvwo2  29435  wlkn0  29694  clwlkcompbp  29855  clwlkclwwlkflem  30079  konigsberglem5  30331  difininv  32592  prmidl2  33522  eulerpartlemgs2  34537  bnj1476  35003  bnj1204  35168  noinfepregs  35289  dfon2lem3  35977  bj-ccinftydisj  37414  nninfnub  37948  ispridl2  38235  rp-isfinite6  43755  fnresfnco  47283