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  7187  fvtp0  7232  frrlem13  8347  brinxper  8778  sdom0  9159  funsnfsupp  9414  sucprcreg  9630  sucprcregOLD  9631  fin23lem40  10459  ffz0iswrd  14716  s4f1o  15101  fsumsplitsnun  15953  lcmcllem  16803  catcone0  17893  prmidl2  21655  lidldvgen  21691  mat1dimbas  22820  pmatcollpw3fi  23136  nbgrssvwo2  29976  wlkn0  30234  clwlkcompbp  30402  clwlkclwwlkflem  30628  konigsberglem5  30890  difininv  33188  eulerpartlemgs2  35095  bnj1476  35560  bnj1204  35725  axprALT2  35829  rncardr1prc  35863  acwer1prc  35865  noinfepregs  35914  dfon2lem3  36738  bj-ccinftydisj  38339  nninfnub  38888  ispridl2  39175  rp-isfinite6  44722  fnresfnco  48326