Theorem syl6rbbr 278

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  baib  942  cad1  1546  necon2abid  2824  reu8  3369  sbc6g  3428  r19.28z  4015  r19.37zv  4019  r19.45zv  4020  r19.44zv  4021  r19.27z  4022  r19.36zv  4024  ralidm  4027  ralsnsg  4163  eldifvsn  4267  ssunsn2  4299  iunconst  4465  iinconst  4466  ordsseleq  5669  ordequn  5745  funssres  5844  fncnv  5876  fresaun  5988  dff1o5  6059  funimass4  6157  fndmdifeq0  6231  fneqeql2  6234  unpreima  6249  dffo3  6282  fnnfpeq0  6349  funfvima  6396  f1eqcocnv  6456  fliftf  6465  isocnv3  6482  isomin  6487  eloprabga  6645  mpt22eqb  6667  elpwun  6869  dfom2  6959  opabex3d  7037  opabex3  7038  f1oweALT  7043  fnwelem  7179  mptsuppd  7205  dfrecs3  7356  oe0m1  7488  oarec  7529  boxcutc  7837  ordunifi  8095  r1fin  8519  rankr1c  8567  iscard  8684  iscard2  8685  cardval2  8700  dfac3  8827  kmlem8  8862  infinf  9267  xrlenlt  9982  ltxrlt  9987  negcon2  10213  mulne0b  10547  dfinfre  10881  crne0  10890  elznn  11270  zmax  11661  zq  11670  elfznelfzo  12439  modmuladdnn0  12576  hashneq0  13016  xpcogend  13561  sqrtneglem  13855  rexfiuz  13935  rexanuz2  13937  sumsplit  14341  fsum2dlem  14343  fsumcom2OLD  14348  fprodcom2OLD  14554  odd2np1  14903  divalgb  14965  gcdcllem2  15060  mrcidb2  16101  fncnvimaeqv  16583  lbsacsbs  18977  islpir2  19072  domnmuln0  19119  mplcoe1  19286  mplcoe5  19289  islinds2  19971  islbs4  19990  mamucl  20026  mavmulcl  20172  mdetunilem8  20244  iscld4  20679  iscon2  21027  kgencn  21169  tx1cn  21222  tx2cn  21223  elmptrab  21440  isfbas  21443  fbfinnfr  21455  cnfcf  21656  fmucndlem  21905  prdsxmslem2  22144  blval2  22177  cnbl0  22387  cnblcld  22388  metcld  22912  ismbf  23203  ismbfcn  23204  itg1val2  23257  itg2split  23322  itg2monolem1  23323  aannenlem1  23887  pilem1  24009  sinq34lt0t  24065  ellogrn  24110  logeftb  24134  gausslemma2dlem1a  24890  ercgrg  25212  isusgra0  25876  usgraop  25879  constr3lem2  26174  ch0pss  27688  h1de2ctlem  27798  adjsym  28076  eigposi  28079  dfadj2  28128  elnlfn  28171  xppreima  28829  1stpreima  28867  2ndpreima  28868  qtophaus  29231  prsdm  29288  prsrn  29289  1stmbfm  29649  2ndmbfm  29650  eulerpartlemn  29770  bnj1454  30166  bnj984  30276  nofulllem1  31101  dffun10  31191  hfext  31460  isfne4b  31506  neifg  31536  taupilem3  32342  topdifinfindis  32370  topdifinffinlem  32371  finxpsuclem  32410  poimirlem23  32602  poimirlem26  32605  cnambfre  32628  0totbnd  32742  19.9alt  33270  cvrval2  33579  cvrnbtwn2  33580  cvrnbtwn4  33584  hlateq  33703  islpln5  33839  islvol5  33883  pmap11  34066  4atex  34380  cdleme0ex2N  34529  cdlemefrs29pre00  34701  diaord  35354  dihmeetlem13N  35626  lcfl1  35799  lcfls1N  35842  mapdpglem3  35982  isnacs2  36287  mrefg3  36289  pw2f1ocnv  36622  acsfn1p  36788  relexp0eq  37012  frege124d  37072  uneqsn  37341  k0004lem1  37465  sbcoreleleq  37766  dffo3f  38359  climreeq  38680  funressnfv  39857  fmtnorec2lem  39992  vtxd0nedgb  40703  vdiscusgrb  40746  s3wwlks2on  41160