Theorem syl6bbr 277

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 213	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	syl6bb 275	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:  3bitr4g  302  bibi2i  326  mtt  353  nbn2  359  rbaibr  944  ifptru  1017  3bior1fd  1430  3biant1d  1433  clelab  2735  eueq3  3348  n0moeu  3893  sbcel12  3935  sbceqg  3936  sbcne12  3938  reldisj  3972  raldifeq  4011  r19.3rz  4014  eldifpr  4152  eldiftp  4175  reusv2lem5  4799  prelpw  4841  otthg  4880  2rbropap  4941  rabxp  5078  elrng  5236  iss  5367  elimasni  5411  eliniseg  5413  xpcan  5489  xpcan2  5490  elpredg  5611  ordelpss  5668  fcnvres  5995  dffv3  6099  funimass4  6157  fndmdif  6229  fneqeql  6233  funimass3  6241  elrnrexdmb  6272  dff4  6281  fnsnb  6337  fconst4  6383  elunirn  6413  f12dfv  6429  riota1  6529  riota2df  6531  f1ocnvfv3  6545  eqfnov  6664  elrnmpt2res  6672  caoftrn  6830  ordsucun  6917  dflim3  6939  dfom2  6959  peano5  6981  opiota  7118  suppssr  7213  mpt2xopovel  7233  brtpos  7248  rntpos  7252  ordgt0ge1  7464  ondif2  7469  oelim2  7562  omabs  7614  iiner  7706  erinxp  7708  qliftfun  7719  ordunifi  8095  elfi2  8203  elfiun  8219  fifo  8221  noinfep  8440  cantnflem1  8469  cantnf  8473  rankonidlem  8574  r1pwALT  8592  pr2nelem  8710  cardalephex  8796  alephinit  8801  dfac5lem4  8832  cflim2  8968  cfsmolem  8975  compssiso  9079  fin1a2lem11  9115  itunisuc  9124  axdclem  9224  brdom6disj  9235  alephreg  9283  fpwwe2lem9  9339  pwfseqlem3  9361  pwfseqlem4  9363  indpi  9608  nqereu  9630  ordpinq  9644  ltanq  9672  ltmnq  9673  suplem2pr  9754  map2psrpr  9810  ssxr  9986  letri3  10002  leltne  10006  ltneg  10407  leneg  10410  suprnub  10865  negiso  10880  elnnnn0  11213  nn0sub  11220  zrevaddcl  11299  znnsub  11300  znn0sub  11301  prime  11334  eluz2  11569  indstr  11632  eluz2b1  11635  qrevaddcl  11686  rpneg  11739  xrleltne  11854  dfle2  11856  dflt2  11857  xrletri3  11861  supxrleub  12028  infxrgelb  12037  ixxin  12063  iccid  12091  elicopnf  12140  iccsplit  12176  fzsplit2  12237  fzsn  12254  fzpr  12266  uzsplit  12281  preduz  12330  fvinim0ffz  12449  injresinj  12451  om2uzf1oi  12614  lt2sqi  12814  le2sqi  12815  hashsdom  13031  hashf1lem1  13096  fz1isolem  13102  prprrab  13112  ccatlcan  13324  ccatrcan  13325  2swrd2eqwrdeq  13544  trclfvcotr  13598  cnpart  13828  limsuplt  14058  rlimresb  14144  mertenslem2  14456  fprod2dlem  14549  sadadd2lem2  15010  saddisjlem  15024  bitsuz  15034  gcddiv  15106  algcvgblem  15128  isprm2lem  15232  isprm3  15234  isprm5  15257  prmreclem5  15462  vdwapun  15516  vdwmc2  15521  ramcl  15571  pwsle  15975  ismre  16073  mreacs  16142  acsfn  16143  iscatd2  16165  cidpropd  16193  dfiso2  16255  oppcsect2  16262  isfunc  16347  setcinv  16563  lubeldm  16804  lubval  16807  glbeldm  16817  glbval  16820  tosso  16859  ipodrsfi  16986  acsfiindd  17000  imasmnd2  17150  submacs  17188  imasgrp2  17353  issubg  17417  resgrpisgrp  17438  subgacs  17452  eqgval  17466  gaorber  17564  symgfix2  17659  psgnran  17758  isslw  17846  sylow2alem2  17856  sylow2a  17857  sylow3lem6  17870  efgcpbllemb  17991  prmcyg  18118  gsum2d2lem  18195  gsumcom2  18197  subgdmdprd  18256  dprd2d2  18266  pgpfac1lem2  18297  pgpfac1lem4  18300  imasring  18442  drngmulne0  18592  lssle0  18771  lssacs  18788  lssats2  18821  lvecvsn0  18930  islpir  19070  isnzr2  19084  zndvds  19717  znleval  19722  znleval2  19723  lindsmm  19986  islinds3  19992  islindf4  19996  eltg2b  20574  discld  20703  opnssneib  20729  cldlp  20764  restbas  20772  leordtvallem1  20824  leordtvallem2  20825  ssidcn  20869  cnprest2  20904  lmss  20912  perfcls  20979  cmpfi  21021  1stccnp  21075  subislly  21094  hausmapdom  21113  locfindis  21143  iskgen3  21162  kgencn  21169  ptpjpre1  21184  xkoccn  21232  txrest  21244  txlm  21261  txkgen  21265  xkopt  21268  xkoinjcn  21300  imasnopn  21303  imasncld  21304  imasncls  21305  qtopcn  21327  kqfeq  21337  isr0  21350  fbfinnfr  21455  trfbas  21458  fbunfip  21483  ufileu  21533  cfinufil  21542  fmid  21574  txflf  21620  fclsrest  21638  alexsubALT  21665  tsmsres  21757  ucnima  21895  fmucndlem  21905  bldisj  22013  xmeter  22048  elbl4  22178  restmetu  22185  dscopn  22188  bl2ioo  22403  isphtpc  22601  tchcph  22844  lmmbr2  22865  lmmbrf  22868  iscau2  22883  iscauf  22886  caucfil  22889  metcld  22912  metcld2  22913  bcthlem1  22929  bcthlem4  22932  cldcss2  23021  ovolgelb  23055  ovoliunlem1  23077  ismbfcn  23204  mbfmax  23222  mbfimaopnlem  23228  i1faddlem  23266  i1fmullem  23267  i1fres  23278  i1fpos  23279  itg1climres  23287  xrge0f  23304  itgresr  23351  iblcnlem1  23360  limcun  23465  dvres  23481  mdegmullem  23642  ply1remlem  23726  plyremlem  23863  vieta1  23871  ulmcau  23953  sineq0  24077  coseq1  24078  ang180lem3  24341  cubic  24376  atandm  24403  atandm2  24404  atandm3  24405  rlimcnp  24492  rlimcnp2  24493  vmappw  24642  dchrelbas3  24763  dchrelbas4  24768  dchrsum2  24793  bposlem6  24814  dchrisumlem3  24980  pntleml  25100  istrkg3ld  25160  tgcgr4  25226  lnrot2  25319  islnopp  25431  islmib  25479  brbtwn2  25585  axsegconlem6  25602  axsegcon  25607  ax5seg  25618  axpasch  25621  axeuclid  25643  axcontlem4  25647  usgrac  25880  elusuhgra  25897  nbgrael  25955  nb3gra2nb  25984  nbcusgra  25992  wlkcomp  26053  trls  26066  istrl2  26068  is2wlk  26095  0pth  26100  0spth  26101  wlkdvspthlem  26137  0crct  26154  0cycl  26155  clwlkcomp  26291  clwlkisclwwlklem0  26316  clwlkisclwwlk  26317  el2wlkonotot0  26399  2wot2wont  26413  usg2spthonot1  26417  2spot2iun2spont  26418  isrusgra  26454  isrusgusrgcl  26460  isrusgrac  26462  0eusgraiff0rgracl  26468  rusgranumwlks  26483  eupath2lem2  26505  vdn1frgrav2  26552  vdgn1frgrav2  26553  usgreg2spot  26594  numclwwlkovgel  26615  nmoolb  27010  nmlno0lem  27032  ubthlem1  27110  ocsh  27526  shle0  27685  eigrei  28077  adjeu  28132  nmoplb  28150  nmfnlb  28167  eleigvec2  28201  nmlnop0iALT  28238  cnlnadjlem5  28314  adjbdln  28326  jplem2  28512  cvbr2  28526  mdsl2bi  28566  chrelat3  28614  disjunsn  28789  ofpreima  28848  funcnvmpt  28851  funcnv5mpt  28852  dfcnv2  28859  gtiso  28861  fpwrelmap  28896  infxrge0glb  28920  xrdifh  28932  fzsplit3  28940  toslublem  28998  tosglblem  29000  isarchi  29067  xrge0tsmsbi  29117  smatrcl  29190  unitdivcld  29275  lmxrge0  29326  isrrext  29372  issibf  29722  eulerpartlemr  29763  eulerpartlemmf  29764  eulerpartlemn  29770  dstfrvunirn  29863  ballotlemfc0  29881  ballotlemfcc  29882  bnj919  30091  bnj976  30102  bnj1542  30181  bnj150  30200  bnj151  30201  bnj607  30240  bnj852  30245  bnj873  30248  bnj938  30261  bnj1171  30322  bnj1388  30355  bnj1489  30378  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem9  30435  kur14  30452  iscvm  30495  mclsax  30720  dfpo2  30898  fundmpss  30910  opelco3  30923  dfon2  30941  nofulllem1  31101  nofulllem2  31102  dfbigcup2  31176  sscoid  31190  funpartfv  31222  dfrdg4  31228  cgr3permute3  31324  segletr  31391  segleantisym  31392  seglelin  31393  fneval  31517  neibastop3  31527  eltail  31539  filnetlem4  31546  bj-hbntbi  31882  bj-sbceqgALT  32089  bj-rest10  32222  topdifinffinlem  32371  isbasisrelowllem1  32379  isbasisrelowllem2  32380  rdgeqoa  32394  finxpreclem4  32407  finxpsuclem  32410  uncf  32558  phpreu  32563  cos2h  32570  tan2h  32571  matunitlindflem1  32575  poimirlem16  32595  poimirlem19  32598  poimirlem23  32602  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  mbfposadd  32627  cnambfre  32628  itg2addnclem  32631  itg2addnc  32634  iblabsnclem  32643  ftc1anclem1  32655  ftc1anclem5  32659  caures  32726  heiborlem3  32782  heiborlem10  32789  elghomOLD  32856  divrngidl  32997  prtlem10  33168  prtlem16  33172  prtlem19  33181  prtex  33183  prter3  33185  islshpat  33322  lcvbr2  33327  lcvbr3  33328  lshpsmreu  33414  isat3  33612  hlrelat5N  33705  islpln5  33839  cdlemblem  34097  paddvaln0N  34105  paddval0  34114  cdlemefrs29bpre1  34703  cdlemefrs29cpre1  34704  cdlemg27b  35002  cdlemg33c  35014  cdlemg33e  35016  diaglbN  35362  cdlemm10N  35425  dicopelval2  35488  dicelval2N  35489  dihopelvalcpre  35555  dihglbcpreN  35607  dih1dimatlem  35636  dihatexv  35645  dvh4dimlem  35750  mapdpglem3  35982  hdmap14lem13  36190  hdmapglem7a  36237  isnacs2  36287  rabrenfdioph  36396  expdiophlem1  36606  pw2f1ocnv  36622  pwfi2f1o  36684  numinfctb  36692  dfacbasgrp  36697  islnr3  36704  subrgacs  36789  sdrgacs  36790  isdomn3  36801  dfhe3  37089  clsk3nimkb  37358  ntrneiiso  37409  ntrneikb  37412  hashnzfzclim  37543  dvconstbi  37555  sbc3orgOLD  37763  sbcel12gOLD  37775  sbcssOLD  37777  rfcnpre3  38215  rfcnpre4  38216  unima  38340  cncfshift  38759  stoweidlem59  38952  iccpartiun  39972  oddm1evenALTV  40124  oddp1evenALTV  40125  oddprmne2  40162  issubgr  40495  nb3gr2nb  40612  uhgrvd00  40750  isrusgr0  40766  1wlkcpr  40833  1wlkcomp  40835  upgr2wlk  40876  upgrf1istrl  40911  clWlkcomp  40986  iswwlksnx  41042  wspthsnwspthsnon  41122  wspniunwspnon  41130  2pthon3v-av  41150  usgr2wspthons3  41167  usgr2wspthon  41168  rusgrnumwwlks  41177  clwlkclwwlklem3  41210  clwlkclwwlk  41211  0Trl  41290  0pth-av  41293  0spth-av  41294  0Crct  41300  0Cycl  41301  eupth2lem2  41387  vdgn1frgrv2  41466  fusgreg2wsp  41500  av-numclwwlkovgel  41519  submgmacs  41594  ismhm0  41595  iscmgmALT  41650  iscsgrpALT  41652  isrnghmmul  41683  elpglem2  42254