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  4642  ftpg  7103  frrlem13  8241  brinxper  8666  sdom0  9040  funsnfsupp  9298  sucprcreg  9512  fin23lem40  10264  ffz0iswrd  14494  s4f1o  14871  fsumsplitsnun  15708  lcmcllem  16556  catcone0  17644  lidldvgen  21324  mat1dimbas  22447  pmatcollpw3fi  22760  nbgrssvwo2  29445  wlkn0  29704  clwlkcompbp  29865  clwlkclwwlkflem  30089  konigsberglem5  30341  difininv  32602  prmidl2  33516  eulerpartlemgs2  34540  bnj1476  35005  bnj1204  35170  axprALT2  35269  noinfepregs  35293  dfon2lem3  35981  bj-ccinftydisj  37543  nninfnub  38086  ispridl2  38373  rp-isfinite6  43963  fnresfnco  47501