Theorem sylbb 197

Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.)

Hypotheses

Ref	Expression
sylbb.1
sylbb.2

Assertion

Ref	Expression
sylbb

Proof of Theorem sylbb

Step	Hyp	Ref	Expression
1		sylbb.1	. 2
2		sylbb.2	. . 3
3	2	biimpi 194	. 2
4	1, 3	sylbi 195	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  bitri  249  trint  4560  pocl  4812  wefrc  4878  fissuni  7845  inf3lem2  8067  rankvalb  8236  xrrebnd  11398  xaddf  11452  elfznelfzob  11916  fsuppmapnn0ub  12101  hashinfxadd  12453  hashfun  12495  wrdeqswrdlsw  12674  clatl  15746  sgrp2nmndlem5  16047  mat1dimelbas  18973  cfinfil  20394  dyadmax  22007  wwlknfi  24738  isch3  26159  nmopun  26933  esumnul  28059  dya2iocnrect  28252  wl-nfeqfb  29990  unitresl  30482  stoweidlem48  31830  fourierdlem42  31931  fourierdlem80  31969  alimp-no-surprise  33196  bnj849  33983  bnj1279  34074  rp-isfinite6  37744  frege70  37961

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 185