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  4668  ftpg  7160  frrlem13  8304  brinxper  8733  sdom0  9107  funsnfsupp  9362  sucprcreg  9578  sucprcregOLD  9579  fin23lem40  10353  ffz0iswrd  14598  s4f1o  14981  fsumsplitsnun  15832  lcmcllem  16679  catcone0  17768  prmidl2  21503  lidldvgen  21539  mat1dimbas  22666  pmatcollpw3fi  22979  nbgrssvwo2  29749  wlkn0  30007  clwlkcompbp  30168  clwlkclwwlkflem  30392  konigsberglem5  30644  difininv  32900  eulerpartlemgs2  34802  bnj1476  35267  bnj1204  35432  axprALT2  35528  noinfepregs  35570  dfon2lem3  36296  bj-ccinftydisj  37898  nninfnub  38443  ispridl2  38730  rp-isfinite6  44285  fnresfnco  47819