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  4673  ftpg  7146  frrlem13  8297  wfrlem5OLD  8327  brinxper  8748  sdom0  9122  funsnfsupp  9404  sucprcreg  9615  fin23lem40  10365  ffz0iswrd  14559  s4f1o  14937  fsumsplitsnun  15771  lcmcllem  16615  catcone0  17699  lidldvgen  21295  mat1dimbas  22410  pmatcollpw3fi  22723  nbgrssvwo2  29341  wlkn0  29601  clwlkcompbp  29764  clwlkclwwlkflem  29985  konigsberglem5  30237  difininv  32498  prmidl2  33456  eulerpartlemgs2  34412  bnj1476  34878  bnj1204  35043  dfon2lem3  35803  bj-ccinftydisj  37231  nninfnub  37775  ispridl2  38062  rp-isfinite6  43542  fnresfnco  47070