Theorem syl6rbbr 291

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 225	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	syl6rbb 289	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  baib  536  cad1  1598  necon2abid  3026  reueubd  3396  reu8  3658  sbc6g  3732  r19.28z  4357  r19.37zv  4361  r19.45zv  4362  r19.44zv  4363  r19.27z  4364  r19.36zv  4366  ralidm  4369  ralsnsg  4513  eldifvsn  4637  ssunsn2  4667  iunconst  4834  iinconst  4835  relsng  5560  opelres  5740  ordsseleq  6095  ordequn  6166  funssres  6268  fncnv  6297  fresaun  6417  dff1o5  6492  funimass4  6598  fndmdifeq0  6679  fneqeql2  6682  unpreima  6698  dffo3  6731  fnnfpeq0  6803  funfvima  6858  f1eqcocnv  6922  fliftf  6931  isocnv3  6948  isomin  6953  eloprabga  7117  mpo2eqb  7139  elpwun  7348  dfom2  7438  opabex3d  7522  opabex3rd  7523  opabex3  7524  f1oweALT  7529  fnwelem  7678  mptsuppd  7704  dfrecs3  7861  oe0m1  7997  oarec  8038  boxcutc  8353  ordunifi  8614  r1fin  9048  rankr1c  9096  iscard  9250  iscard2  9251  cardval2  9266  dfac3  9393  kmlem8  9429  infinf  9834  xrlenlt  10553  ltxrlt  10558  negcon2  10787  mulne0b  11129  dfinfre  11470  crne0  11479  elznn  11845  zmax  12194  zqOLD  12204  elfznelfzo  12992  modmuladdnn0  13133  hashneq0  13575  xpcogend  14168  sqrtneglem  14460  rexfiuz  14541  rexanuz2  14543  sumsplit  14956  fsum2dlem  14958  odd2np1  15523  divalgb  15588  gcdcllem2  15682  mrcidb2  16718  fncnvimaeqv  17199  acsfn1p  19268  lbsacsbs  19618  islpir2  19713  domnmuln0  19760  mplcoe1  19933  mplcoe5  19936  islinds2  20639  islbs4  20658  mamucl  20694  mavmulcl  20840  mdetunilem8  20912  iscld4  21357  isconn2  21706  kgencn  21848  tx1cn  21901  tx2cn  21902  elmptrab  22119  isfbas  22121  fbfinnfr  22133  cnfcf  22334  fmucndlem  22583  prdsxmslem2  22822  blval2  22855  cnbl0  23065  cnblcld  23066  metcld  23592  ismbf  23912  ismbfcn  23913  itg1val2  23968  itg2split  24033  itg2monolem1  24034  aannenlem1  24600  pilem1  24722  sinq34lt0t  24778  ellogrn  24824  logeftb  24848  gausslemma2dlem1a  25623  ercgrg  25985  elntg2  26454  usgredgffibi  26789  vtxd0nedgb  26953  vdiscusgrb  26995  upgrspthswlk  27206  s3wwlks2on  27422  frgrncvvdeqlem2  27771  ch0pss  28913  h1de2ctlem  29023  adjsym  29301  eigposi  29304  dfadj2  29353  elnlfn  29396  xppreima  30084  1stpreima  30130  2ndpreima  30131  creq0  30159  hashgt1  30214  lindflbs  30586  qtophaus  30717  prsdm  30774  prsrn  30775  1stmbfm  31135  2ndmbfm  31136  eulerpartlemn  31256  reprdifc  31515  circlemeth  31528  bnj1454  31730  bnj984  31840  dffun10  32985  hfext  33254  isfne4b  33299  neifg  33329  taupilem3  34150  topdifinfindis  34177  topdifinffinlem  34178  finxpsuclem  34228  nlpineqsn  34239  wl-dfrabf  34414  poimirlem23  34465  poimirlem26  34468  cnambfre  34490  0totbnd  34602  opelvvdif  35071  inecmo  35160  brxrn  35176  brin2  35207  eleccossin  35273  dffunsALTV2  35467  dffunsALTV3  35468  dffunsALTV4  35469  elfunsALTV2  35476  elfunsALTV3  35477  elfunsALTV4  35478  elfunsALTV5  35479  dfdisjs2  35492  eldisjs2  35506  cvrval2  35960  cvrnbtwn2  35961  cvrnbtwn4  35965  hlateq  36085  islpln5  36221  islvol5  36265  pmap11  36448  4atex  36762  cdleme0ex2N  36910  cdlemefrs29pre00  37081  diaord  37733  dihmeetlem13N  38005  lcfl1  38178  lcfls1N  38221  mapdpglem3  38361  isnacs2  38807  mrefg3  38809  pw2f1ocnv  39138  relexp0eq  39550  frege124d  39610  uneqsn  39877  k0004lem1  40001  sbcoreleleq  40427  dffo3f  40997  climreeq  41455  funressnfv  42814  fmtnorec2lem  43206  eenglngeehlnmlem1  44225  eenglngeehlnmlem2  44226  rrx2linest2  44232  itsclinecirc0b  44262