Theorem sylbb2 237

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 227	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	sylbi 216	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  rexprg  4633  ftpg  7037  frrlem13  8123  wfrlem5OLD  8153  sdom0  8904  funsnfsupp  9161  sucprcreg  9369  fin23lem40  10116  ffz0iswrd  14253  s4f1o  14640  fsumsplitsnun  15476  lcmcllem  16310  catcone0  17405  lidldvgen  20535  mat1dimbas  21630  pmatcollpw3fi  21943  nbgrssvwo2  27738  wlkn0  27997  clwlkcompbp  28159  clwlkclwwlkflem  28377  konigsberglem5  28629  difininv  30873  prmidl2  31625  eulerpartlemgs2  32356  bnj1476  32836  bnj1204  33001  dfon2lem3  33770  bj-ccinftydisj  35393  nninfnub  35918  ispridl2  36205  rp-isfinite6  41132  fnresfnco  44546