Theorem sylbb2 240

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  rexprg  4655  ftpg  7135  frrlem13  8274  brinxper  8703  sdom0  9077  funsnfsupp  9335  sucprcreg  9551  sucprcregOLD  9552  fin23lem40  10305  ffz0iswrd  14551  s4f1o  14928  fsumsplitsnun  15765  lcmcllem  16613  catcone0  17702  lidldvgen  21384  mat1dimbas  22512  pmatcollpw3fi  22825  nbgrssvwo2  29509  wlkn0  29767  clwlkcompbp  29928  clwlkclwwlkflem  30152  konigsberglem5  30404  difininv  32665  prmidl2  33588  eulerpartlemgs2  34638  bnj1476  35106  bnj1204  35271  axprALT2  35369  noinfepregs  35393  dfon2lem3  36097  bj-ccinftydisj  37669  nninfnub  38214  ispridl2  38501  rp-isfinite6  44058  fnresfnco  47599