Theorem syl6rbbr 292

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
syl6rbbr.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
syl6rbbr.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
syl6rbbr	⊢ (𝜑 → (𝜃 ↔ 𝜓))

Proof of Theorem syl6rbbr

Step	Hyp	Ref	Expression
1		syl6rbbr.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		syl6rbbr.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	bicomi 226	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	syl6rbb 290	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  baib  538  cad1  1613  necon2abid  3058  reueubd  3436  reu8  3723  sbc6g  3800  r19.28z  4442  r19.37zv  4446  r19.45zv  4447  r19.44zv  4448  r19.27z  4449  r19.36zv  4451  ralidm  4454  ralsnsg  4601  eldifvsn  4723  ssunsn2  4753  iunconst  4920  iinconst  4921  iuneqconst  4922  relsng  5668  opelres  5853  ordsseleq  6214  ordequn  6285  funssres  6392  fncnv  6421  fresaun  6543  dff1o5  6618  funimass4  6724  fndmdifeq0  6808  fneqeql2  6811  unpreima  6827  dffo3  6862  fnnfpeq0  6934  funfvima  6986  f1eqcocnv  7051  fliftf  7062  isocnv3  7079  isomin  7084  eloprabga  7255  mpo2eqb  7277  elpwun  7485  dfom2  7576  opabex3d  7660  opabex3rd  7661  opabex3  7662  f1oweALT  7667  fnwelem  7819  mptsuppd  7847  dfrecs3  8003  oe0m1  8140  oarec  8182  boxcutc  8499  ordunifi  8762  r1fin  9196  rankr1c  9244  iscard  9398  iscard2  9399  cardval2  9414  dfac3  9541  kmlem8  9577  infinf  9982  xrlenlt  10700  ltxrlt  10705  negcon2  10933  mulne0b  11275  dfinfre  11616  crne0  11625  elznn  11991  zmax  12339  elfznelfzo  13136  modmuladdnn0  13277  hashneq0  13719  xpcogend  14328  sqrtneglem  14620  rexfiuz  14701  rexanuz2  14703  sumsplit  15117  fsum2dlem  15119  odd2np1  15684  divalgb  15749  gcdcllem2  15843  mrcidb2  16883  fncnvimaeqv  17364  acsfn1p  19572  lbsacsbs  19922  islpir2  20018  domnmuln0  20065  mplcoe1  20240  mplcoe5  20243  islinds2  20951  islbs4  20970  mamucl  21004  mavmulcl  21150  mdetunilem8  21222  iscld4  21667  isconn2  22016  kgencn  22158  tx1cn  22211  tx2cn  22212  elmptrab  22429  isfbas  22431  fbfinnfr  22443  cnfcf  22644  fmucndlem  22894  prdsxmslem2  23133  blval2  23166  cnbl0  23376  cnblcld  23377  metcld  23903  ismbf  24223  ismbfcn  24224  itg1val2  24279  itg2split  24344  itg2monolem1  24345  aannenlem1  24911  pilem1  25033  sinq34lt0t  25089  ellogrn  25137  logeftb  25161  gausslemma2dlem1a  25935  ercgrg  26297  elntg2  26765  usgredgffibi  27100  vtxd0nedgb  27264  vdiscusgrb  27306  upgrspthswlk  27513  s3wwlks2on  27729  clwwlknonwwlknonb  27879  frgrncvvdeqlem2  28073  ch0pss  29216  h1de2ctlem  29326  adjsym  29604  eigposi  29607  dfadj2  29656  elnlfn  29699  xppreima  30388  1stpreima  30436  2ndpreima  30437  creq0  30465  hashgt1  30524  qusxpid  30923  lindflbs  30935  lsmsnorb  30940  qtophaus  31095  prsdm  31152  prsrn  31153  1stmbfm  31513  2ndmbfm  31514  eulerpartlemn  31634  reprdifc  31893  circlemeth  31906  bnj1454  32109  bnj984  32219  dffun10  33370  hfext  33639  isfne4b  33684  neifg  33714  taupilem3  34594  topdifinfindis  34621  topdifinffinlem  34622  finxpsuclem  34672  nlpineqsn  34683  wl-dfrabf  34858  poimirlem23  34909  poimirlem26  34912  cnambfre  34934  0totbnd  35045  opelvvdif  35514  inecmo  35603  brxrn  35620  brin2  35651  eleccossin  35717  dffunsALTV2  35911  dffunsALTV3  35912  dffunsALTV4  35913  elfunsALTV2  35920  elfunsALTV3  35921  elfunsALTV4  35922  elfunsALTV5  35923  dfdisjs2  35936  eldisjs2  35950  cvrval2  36404  cvrnbtwn2  36405  cvrnbtwn4  36409  hlateq  36529  islpln5  36665  islvol5  36709  pmap11  36892  4atex  37206  cdleme0ex2N  37354  cdlemefrs29pre00  37525  diaord  38177  dihmeetlem13N  38449  lcfl1  38622  lcfls1N  38665  mapdpglem3  38805  isnacs2  39296  mrefg3  39298  pw2f1ocnv  39627  relexp0eq  40039  frege124d  40099  uneqsn  40366  k0004lem1  40490  sbcoreleleq  40862  dffo3f  41431  climreeq  41887  funressnfv  43272  fmtnorec2lem  43698  eenglngeehlnmlem1  44718  eenglngeehlnmlem2  44719  rrx2linest2  44725  itsclinecirc0b  44755