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  1617  necon2abid  3060  reueubd  3438  reu8  3726  sbc6g  3803  r19.28z  4445  r19.37zv  4449  r19.45zv  4450  r19.44zv  4451  r19.27z  4452  r19.36zv  4454  ralidm  4457  ralsnsg  4610  eldifvsn  4732  ssunsn2  4762  iunconst  4930  iinconst  4931  iuneqconst  4932  relsng  5676  opelres  5861  ordsseleq  6222  ordequn  6293  funssres  6400  fncnv  6429  fresaun  6551  dff1o5  6626  funimass4  6732  fndmdifeq0  6816  fneqeql2  6819  unpreima  6835  dffo3  6870  fnnfpeq0  6942  funfvima  6994  f1eqcocnv  7059  fliftf  7070  isocnv3  7087  isomin  7092  eloprabga  7263  mpo2eqb  7285  elpwun  7493  dfom2  7584  opabex3d  7668  opabex3rd  7669  opabex3  7670  f1oweALT  7675  fnwelem  7827  mptsuppd  7855  dfrecs3  8011  oe0m1  8148  oarec  8190  boxcutc  8507  ordunifi  8770  r1fin  9204  rankr1c  9252  iscard  9406  iscard2  9407  cardval2  9422  dfac3  9549  kmlem8  9585  infinf  9990  xrlenlt  10708  ltxrlt  10713  negcon2  10941  mulne0b  11283  dfinfre  11624  crne0  11633  elznn  12000  zmax  12348  elfznelfzo  13145  modmuladdnn0  13286  hashneq0  13728  xpcogend  14336  sqrtneglem  14628  rexfiuz  14709  rexanuz2  14711  sumsplit  15125  fsum2dlem  15127  odd2np1  15692  divalgb  15757  gcdcllem2  15851  mrcidb2  16891  fncnvimaeqv  17372  acsfn1p  19580  lbsacsbs  19930  islpir2  20026  domnmuln0  20073  mplcoe1  20248  mplcoe5  20251  islinds2  20959  islbs4  20978  mamucl  21012  mavmulcl  21158  mdetunilem8  21230  iscld4  21675  isconn2  22024  kgencn  22166  tx1cn  22219  tx2cn  22220  elmptrab  22437  isfbas  22439  fbfinnfr  22451  cnfcf  22652  fmucndlem  22902  prdsxmslem2  23141  blval2  23174  cnbl0  23384  cnblcld  23385  metcld  23911  ismbf  24231  ismbfcn  24232  itg1val2  24287  itg2split  24352  itg2monolem1  24353  aannenlem1  24919  pilem1  25041  sinq34lt0t  25097  ellogrn  25145  logeftb  25169  gausslemma2dlem1a  25943  ercgrg  26305  elntg2  26773  usgredgffibi  27108  vtxd0nedgb  27272  vdiscusgrb  27314  upgrspthswlk  27521  s3wwlks2on  27737  clwwlknonwwlknonb  27887  frgrncvvdeqlem2  28081  ch0pss  29224  h1de2ctlem  29334  adjsym  29612  eigposi  29615  dfadj2  29664  elnlfn  29707  xppreima  30396  1stpreima  30444  2ndpreima  30445  creq0  30473  hashgt1  30532  qusxpid  30930  lindflbs  30942  lsmsnorb  30947  qtophaus  31102  prsdm  31159  prsrn  31160  1stmbfm  31520  2ndmbfm  31521  eulerpartlemn  31641  reprdifc  31900  circlemeth  31913  bnj1454  32116  bnj984  32226  dffun10  33377  hfext  33646  isfne4b  33691  neifg  33721  taupilem3  34602  topdifinfindis  34629  topdifinffinlem  34630  finxpsuclem  34680  nlpineqsn  34691  wl-dfrabf  34866  poimirlem23  34917  poimirlem26  34920  cnambfre  34942  0totbnd  35053  opelvvdif  35522  inecmo  35611  brxrn  35628  brin2  35659  eleccossin  35725  dffunsALTV2  35919  dffunsALTV3  35920  dffunsALTV4  35921  elfunsALTV2  35928  elfunsALTV3  35929  elfunsALTV4  35930  elfunsALTV5  35931  dfdisjs2  35944  eldisjs2  35958  cvrval2  36412  cvrnbtwn2  36413  cvrnbtwn4  36417  hlateq  36537  islpln5  36673  islvol5  36717  pmap11  36900  4atex  37214  cdleme0ex2N  37362  cdlemefrs29pre00  37533  diaord  38185  dihmeetlem13N  38457  lcfl1  38630  lcfls1N  38673  mapdpglem3  38813  isnacs2  39310  mrefg3  39312  pw2f1ocnv  39641  relexp0eq  40053  frege124d  40113  uneqsn  40380  k0004lem1  40504  sbcoreleleq  40876  dffo3f  41445  climreeq  41901  funressnfv  43285  fmtnorec2lem  43711  eenglngeehlnmlem1  44731  eenglngeehlnmlem2  44732  rrx2linest2  44738  itsclinecirc0b  44768