Theorem sylbb2 241

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  rexprg  4661  ftpg  7157  fvtp0  7203  frrlem13  8301  brinxper  8730  sdom0  9111  funsnfsupp  9366  sucprcreg  9582  sucprcregOLD  9583  fin23lem40  10357  ffz0iswrd  14610  s4f1o  14993  fsumsplitsnun  15845  lcmcllem  16692  catcone0  17781  prmidl2  21535  lidldvgen  21571  mat1dimbas  22700  pmatcollpw3fi  23016  nbgrssvwo2  29830  wlkn0  30088  clwlkcompbp  30256  clwlkclwwlkflem  30482  konigsberglem5  30744  difininv  33000  eulerpartlemgs2  34899  bnj1476  35364  bnj1204  35529  axprALT2  35625  noinfepregs  35667  dfon2lem3  36370  bj-ccinftydisj  37973  nninfnub  38509  ispridl2  38796  rp-isfinite6  44366  fnresfnco  47937