Theorem syl6bbr 291

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem syl6bbr

Step	Hyp	Ref	Expression
1		syl6bbr.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		syl6bbr.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	bicomi 226	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	syl6bb 289	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:  3bitr4g  316  bibi2i  340  mtt  367  nbn2  373  ifptru  1068  3bior1fd  1471  3biant1d  1474  clelab  2958  eueq3  3702  n0moeu  4316  sbcel12  4360  sbceqg  4361  sbcne12  4364  reldisj  4402  raldifeq  4439  r19.3rz  4442  eldifpr  4597  reusngf  4612  rexreusng  4617  eldiftp  4624  reusv2lem5  5303  prelpw  5339  otthg  5377  2rbropap  5451  rabxp  5600  pwvrel  5602  elrng  5762  iss  5903  elimasni  5956  eliniseg  5958  idrefALT  5973  xpcan  6033  xpcan2  6034  elpredg  6162  ordelpss  6219  fcnvres  6556  dffv3  6666  funimass4  6730  unima  6739  fndmdif  6812  fneqeql  6816  funimass3  6824  elrnrexdmb  6856  dff4  6867  fnsnb  6928  fconst4  6977  elunirn  7010  f12dfv  7030  riota1  7135  riota2df  7137  f1ocnvfv3  7152  eqfnov  7280  elrnmpores  7288  caoftrn  7444  ordsucun  7540  dflim3  7562  dfom2  7582  peano5  7605  opiota  7757  suppssr  7861  mpoxopovel  7886  brtpos  7901  rntpos  7905  ordgt0ge1  8122  ondif2  8127  oelim2  8221  omabs  8274  iiner  8369  erinxp  8371  qliftfun  8382  mapdm0  8421  ordunifi  8768  elfi2  8878  elfiun  8894  fifo  8896  noinfep  9123  cantnflem1  9152  cantnf  9156  rankonidlem  9257  r1pwALT  9275  pr2nelem  9430  cardalephex  9516  alephinit  9521  dfac5lem4  9552  cflim2  9685  cfsmolem  9692  compssiso  9796  fin1a2lem11  9832  itunisuc  9841  axdclem  9941  brdom6disj  9954  alephreg  10004  fpwwe2lem9  10060  pwfseqlem3  10082  pwfseqlem4  10084  indpi  10329  nqereu  10351  ordpinq  10365  ltanq  10393  ltmnq  10394  suplem2pr  10475  map2psrpr  10532  ssxr  10710  leltne  10730  ltneg  11140  leneg  11143  suprnub  11606  negiso  11621  elnnnn0  11941  nn0sub  11948  zrevaddcl  12028  znnsub  12029  znn0sub  12030  prime  12064  eluz2  12250  indstr  12317  eluz2b1  12320  qrevaddcl  12371  rpneg  12422  xrleltne  12539  dfle2  12541  dflt2  12542  supxrleub  12720  infxrgelb  12729  ixxin  12756  iccid  12784  elicopnf  12834  iccsplit  12872  fzsplit2  12933  fzsn  12950  fzpr  12963  uzsplit  12980  preduz  13030  fvinim0ffz  13157  injresinj  13159  om2uzf1oi  13322  lt2sqi  13553  le2sqi  13554  hashsdom  13743  hashf1lem1  13814  fz1isolem  13820  prprrab  13832  ccatlcan  14080  ccatrcan  14081  s3eq3seq  14301  2swrd2eqwrdeq  14315  trclfvcotr  14369  cnpart  14599  limsuplt  14836  rlimresb  14922  mertenslem2  15241  fprod2dlem  15334  sadadd2lem2  15799  saddisjlem  15813  bitsuz  15823  gcddiv  15899  algcvgblem  15921  isprm3  16027  isprm5  16051  prmreclem5  16256  vdwapun  16310  vdwmc2  16315  ramcl  16365  pwsle  16765  ismre  16861  mreacs  16929  acsfn  16930  iscatd2  16952  cidpropd  16980  dfiso2  17042  oppcsect2  17049  isfunc  17134  setcinv  17350  lubeldm  17591  lubval  17594  glbeldm  17604  glbval  17607  tosso  17646  ipodrsfi  17773  acsfiindd  17787  imasmnd2  17948  resmndismnd  17973  submacs  17991  imasgrp2  18214  issubg  18279  resgrpisgrp  18300  subgacs  18313  eqgval  18329  gaorber  18438  symgfix2  18544  psgnran  18643  isslw  18733  sylow2alem2  18743  sylow2a  18744  sylow3lem6  18757  efgcpbllemb  18881  prmcyg  19014  gsum2d2lem  19093  gsumcom2  19095  subgdmdprd  19156  dprd2d2  19166  pgpfac1lem2  19197  pgpfac1lem4  19200  imasring  19369  drngmulne0  19524  subrgacs  19579  sdrgacs  19580  lssle0  19721  lssacs  19739  lssats2  19772  lvecvsn0  19881  islpir  20022  isnzr2  20036  zndvds  20696  znleval  20701  znleval2  20702  lindsmm  20972  islinds3  20978  islindf4  20982  eltg2b  21567  discld  21697  opnssneib  21723  cldlp  21758  restbas  21766  leordtvallem1  21818  leordtvallem2  21819  ssidcn  21863  cnprest2  21898  lmss  21906  perfcls  21973  cmpfi  22016  1stccnp  22070  subislly  22089  hausmapdom  22108  locfindis  22138  iskgen3  22157  kgencn  22164  ptpjpre1  22179  xkoccn  22227  txrest  22239  txlm  22256  txkgen  22260  xkopt  22263  xkoinjcn  22295  imasnopn  22298  imasncld  22299  imasncls  22300  qtopcn  22322  kqfeq  22332  isr0  22345  fbfinnfr  22449  trfbas  22452  fbunfip  22477  ufileu  22527  cfinufil  22536  fmid  22568  txflf  22614  fclsrest  22632  alexsubALT  22659  tsmsres  22752  ucnima  22890  fmucndlem  22900  bldisj  23008  xmeter  23043  elbl4  23173  restmetu  23180  dscopn  23183  bl2ioo  23400  isphtpc  23598  tcphcph  23840  lmmbr2  23862  lmmbrf  23865  iscau2  23880  iscauf  23883  caucfil  23886  metcld  23909  metcld2  23910  bcthlem1  23927  bcthlem4  23930  cldcss2  24045  ovolgelb  24081  ovoliunlem1  24103  ismbfcn  24230  mbfmax  24250  mbfimaopnlem  24256  i1faddlem  24294  i1fmullem  24295  i1fres  24306  i1fpos  24307  itg1climres  24315  xrge0f  24332  itgresr  24379  iblcnlem1  24388  limcun  24493  dvres  24509  mdegmullem  24672  ply1remlem  24756  plyremlem  24893  vieta1  24901  ulmcau  24983  sineq0  25109  coseq1  25110  ang180lem3  25389  cubic  25427  atandm  25454  atandm2  25455  atandm3  25456  rlimcnp  25543  rlimcnp2  25544  vmappw  25693  dchrelbas3  25814  dchrelbas4  25819  dchrsum2  25844  bposlem6  25865  2sqreuopltb  26041  2sqreuopnnltb  26043  dchrisumlem3  26067  pntleml  26187  istrkg3ld  26247  tgcgr4  26317  lnrot2  26410  islnopp  26525  islmib  26573  brbtwn2  26691  axsegconlem6  26708  axsegcon  26713  ax5seg  26724  axpasch  26727  axeuclid  26749  axcontlem4  26753  elntg2  26771  issubgr  27053  nb3gr2nb  27166  uhgrvd00  27316  isrusgr0  27348  wlkcpr  27410  wlkcomp  27412  upgr2wlk  27450  upgrf1istrl  27485  clwlkcomp  27560  clwlkcompbp  27563  iswwlksnx  27618  wspthsnwspthsnon  27695  wspniunwspnon  27702  2pthon3v  27722  usgr2wspthons3  27743  usgr2wspthon  27744  rusgrnumwwlks  27753  clwlkclwwlklem3  27779  clwlkclwwlk  27780  clwwlknonwwlknonb  27885  0pth  27904  eupth2lem2  27998  vdgn1frgrv2  28075  fusgreg2wsp  28115  clwwlknonclwlknonf1o  28141  dlwwlknondlwlknonf1o  28144  wlkl0  28146  nmoolb  28548  nmlno0lem  28570  ubthlem1  28647  ocsh  29060  shle0  29219  eigrei  29611  adjeu  29666  nmoplb  29684  nmfnlb  29701  eleigvec2  29735  nmlnop0iALT  29772  cnlnadjlem5  29848  adjbdln  29860  jplem2  30046  cvbr2  30060  mdsl2bi  30100  chrelat3  30148  sq2reunnltb  30248  rmounid  30259  eqsnd  30289  nelpr  30291  disjunsn  30344  ofpreima  30410  funcnvmpt  30412  funcnv5mpt  30413  dfcnv2  30422  gtiso  30436  fpwrelmap  30469  infxrge0glb  30489  xrdifh  30503  fzsplit3  30517  swrdrn3  30629  toslublem  30654  tosglblem  30656  xrge0tsmsbi  30693  cntzun  30695  isarchi  30811  lsmsnorb  30945  isprmidl  30955  smatrcl  31061  unitdivcld  31144  lmxrge0  31195  isrrext  31241  issibf  31591  eulerpartlemr  31632  eulerpartlemmf  31633  eulerpartlemn  31639  dstfrvunirn  31732  ballotlemfc0  31750  ballotlemfcc  31751  reprsuc  31886  reprpmtf1o  31897  reprdifc  31898  bnj919  32038  bnj976  32049  bnj1542  32129  bnj150  32148  bnj151  32149  bnj607  32188  bnj852  32193  bnj873  32196  bnj938  32209  bnj1171  32272  bnj1388  32305  bnj1489  32328  usgrgt2cycl  32377  subfacp1lem3  32429  subfacp1lem5  32431  erdszelem9  32446  kur14  32463  iscvm  32506  satf0op  32624  mclsax  32816  dfpo2  32991  elintfv  33007  fundmpss  33009  opelco3  33018  dfon2  33037  noetalem3  33219  dfbigcup2  33360  sscoid  33374  funpartfv  33406  dfrdg4  33412  cgr3permute3  33508  segletr  33575  segleantisym  33576  seglelin  33577  fneval  33700  neibastop3  33710  eltail  33722  filnetlem4  33729  bj-hbntbi  34038  bj-sbceqgALT  34222  bj-rest10  34382  bj-0int  34396  bj-imdirid  34478  topdifinffinlem  34631  isbasisrelowllem1  34639  isbasisrelowllem2  34640  rdgeqoa  34654  finxpreclem4  34678  finxpsuclem  34681  uncf  34886  phpreu  34891  cos2h  34898  tan2h  34899  matunitlindflem1  34903  poimirlem16  34923  poimirlem19  34926  poimirlem23  34930  poimirlem24  34931  poimirlem26  34933  poimirlem27  34934  mbfposadd  34954  cnambfre  34955  itg2addnclem  34958  itg2addnc  34961  iblabsnclem  34970  ftc1anclem1  34982  ftc1anclem5  34986  caures  35050  heiborlem3  35106  heiborlem10  35113  elghomOLD  35180  divrngidl  35321  eqrelf  35532  brvbrvvdif  35540  eldmqsres2  35559  exanres  35567  ssrel3  35571  relcnveq  35594  iss2  35616  ecinn0  35622  brxrn2  35642  ecxrn  35654  eldmcoss2  35714  eldm1cossres  35715  elrelsrel  35742  elrelscnveq  35747  elcoeleqvrelsrel  35846  brredundsredund  35877  brdmqssqs  35897  cnvepresdmqss  35901  eldmqs1cossres  35908  brerser  35925  erim2  35926  eleldisjseldisj  35977  prtlem10  36016  prtlem16  36020  prtlem19  36029  prtex  36031  prter3  36033  islshpat  36168  lcvbr2  36173  lcvbr3  36174  lshpsmreu  36260  isat3  36458  hlrelat5N  36552  islpln5  36686  cdlemblem  36944  paddvaln0N  36952  paddval0  36961  cdlemefrs29bpre1  37548  cdlemefrs29cpre1  37549  cdlemg27b  37847  cdlemg33c  37859  cdlemg33e  37861  diaglbN  38206  cdlemm10N  38269  dicopelval2  38332  dicelval2N  38333  dihopelvalcpre  38399  dihglbcpreN  38451  dih1dimatlem  38480  dihatexv  38489  dvh4dimlem  38594  mapdpglem3  38826  hdmap14lem13  39031  hdmapglem7a  39078  fnsnbt  39140  isnacs2  39323  rabrenfdioph  39431  expdiophlem1  39638  pw2f1ocnv  39654  pwfi2f1o  39716  numinfctb  39723  dfacbasgrp  39728  islnr3  39735  isdomn3  39824  dfhe3  40141  clsk3nimkb  40410  ntrneiiso  40461  ntrneikb  40464  scottabf  40596  mnuunid  40633  hashnzfzclim  40674  dvconstbi  40686  sbcoreleleqVD  41213  rfcnpre3  41310  rfcnpre4  41311  cncfshift  42177  stoweidlem59  42364  dfafv23  43472  nelbrnel  43495  elsetpreimafvrab  43574  iccpartiun  43614  prproropf1olem0  43684  prprelb  43698  prprspr2  43700  reuprpr  43705  oddm1evenALTV  43860  oddp1evenALTV  43861  oddprmne2  43900  fpprel  43913  submgmacs  44091  ismhm0  44092  iscmgmALT  44151  iscsgrpALT  44153  isrnghmmul  44184  elpglem2  44834