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  4654  ftpg  7161  fvtp0  7207  frrlem13  8320  brinxper  8751  sdom0  9132  funsnfsupp  9388  sucprcreg  9604  sucprcregOLD  9605  fin23lem40  10433  ffz0iswrd  14690  s4f1o  15075  fsumsplitsnun  15927  lcmcllem  16777  catcone0  17867  prmidl2  21628  lidldvgen  21664  mat1dimbas  22793  pmatcollpw3fi  23109  nbgrssvwo2  29949  wlkn0  30207  clwlkcompbp  30375  clwlkclwwlkflem  30601  konigsberglem5  30863  difininv  33161  eulerpartlemgs2  35059  bnj1476  35524  bnj1204  35689  axprALT2  35787  rncardr1prc  35815  acwer1prc  35817  noinfepregs  35858  dfon2lem3  36640  bj-ccinftydisj  38228  nninfnub  38779  ispridl2  39066  rp-isfinite6  44613  fnresfnco  48205