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  4658  ftpg  7152  fvtp0  7198  frrlem13  8300  brinxper  8731  sdom0  9112  funsnfsupp  9368  sucprcreg  9584  sucprcregOLD  9585  fin23lem40  10410  ffz0iswrd  14666  s4f1o  15049  fsumsplitsnun  15901  lcmcllem  16751  catcone0  17841  prmidl2  21602  lidldvgen  21638  mat1dimbas  22767  pmatcollpw3fi  23083  nbgrssvwo2  29925  wlkn0  30183  clwlkcompbp  30351  clwlkclwwlkflem  30577  konigsberglem5  30839  difininv  33095  eulerpartlemgs2  34995  bnj1476  35460  bnj1204  35625  axprALT2  35713  noinfepregs  35774  dfon2lem3  36517  bj-ccinftydisj  38102  nninfnub  38653  ispridl2  38940  rp-isfinite6  44477  fnresfnco  48055