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 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  rexprg  4659  ftpg  7143  frrlem13  8283  brinxper  8712  sdom0  9085  funsnfsupp  9340  sucprcreg  9556  sucprcregOLD  9557  fin23lem40  10323  ffz0iswrd  14566  s4f1o  14943  fsumsplitsnun  15794  lcmcllem  16642  catcone0  17731  prmidl2  21425  lidldvgen  21459  mat1dimbas  22586  pmatcollpw3fi  22899  nbgrssvwo2  29617  wlkn0  29875  clwlkcompbp  30036  clwlkclwwlkflem  30260  konigsberglem5  30512  difininv  32769  eulerpartlemgs2  34682  bnj1476  35147  bnj1204  35312  axprALT2  35412  noinfepregs  35436  dfon2lem3  36141  bj-ccinftydisj  37712  nninfnub  38257  ispridl2  38544  rp-isfinite6  44101  fnresfnco  47634