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  4650  ftpg  7089  frrlem13  8228  brinxper  8651  sdom0  9022  funsnfsupp  9276  sucprcreg  9490  fin23lem40  10239  ffz0iswrd  14445  s4f1o  14822  fsumsplitsnun  15659  lcmcllem  16504  catcone0  17590  lidldvgen  21269  mat1dimbas  22385  pmatcollpw3fi  22698  nbgrssvwo2  29338  wlkn0  29597  clwlkcompbp  29758  clwlkclwwlkflem  29979  konigsberglem5  30231  difininv  32492  prmidl2  33401  eulerpartlemgs2  34388  bnj1476  34854  bnj1204  35019  dfon2lem3  35818  bj-ccinftydisj  37246  nninfnub  37790  ispridl2  38077  rp-isfinite6  43550  fnresfnco  47071