Theorem syl6bbr 290

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 225	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	syl6bb 288	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:  3bitr4g  315  bibi2i  339  mtt  366  nbn2  372  ifptru  1066  3bior1fd  1467  3biant1d  1470  clelab  2930  eueq3  3638  n0moeu  4236  sbcel12  4280  sbceqg  4281  sbcne12  4284  reldisj  4316  raldifeq  4353  r19.3rz  4356  eldifpr  4502  reusngf  4519  rexreusng  4524  eldiftp  4531  reusv2lem5  5194  prelpw  5230  otthg  5269  2rbropap  5339  rabxp  5488  elrng  5648  iss  5784  elimasni  5832  eliniseg  5834  idrefALT  5849  xpcan  5909  xpcan2  5910  elpredg  6037  ordelpss  6094  fcnvres  6424  dffv3  6534  funimass4  6598  fndmdif  6677  fneqeql  6681  funimass3  6689  elrnrexdmb  6721  dff4  6730  fnsnb  6791  fconst4  6843  elunirn  6875  f12dfv  6895  riota1  6995  riota2df  6997  f1ocnvfv3  7012  eqfnov  7136  elrnmpores  7144  caoftrn  7302  ordsucun  7396  dflim3  7418  dfom2  7438  peano5  7461  opiota  7613  suppssr  7712  mpoxopovel  7737  brtpos  7752  rntpos  7756  ordgt0ge1  7973  ondif2  7978  oelim2  8071  omabs  8124  iiner  8219  erinxp  8221  qliftfun  8232  mapdm0  8271  ordunifi  8614  elfi2  8724  elfiun  8740  fifo  8742  noinfep  8969  cantnflem1  8998  cantnf  9002  rankonidlem  9103  r1pwALT  9121  pr2nelem  9276  cardalephex  9362  alephinit  9367  dfac5lem4  9398  cflim2  9531  cfsmolem  9538  compssiso  9642  fin1a2lem11  9678  itunisuc  9687  axdclem  9787  brdom6disj  9800  alephreg  9850  fpwwe2lem9  9906  pwfseqlem3  9928  pwfseqlem4  9930  indpi  10175  nqereu  10197  ordpinq  10211  ltanq  10239  ltmnq  10240  suplem2pr  10321  map2psrpr  10378  ssxr  10557  leltne  10577  ltneg  10988  leneg  10991  suprnub  11454  negiso  11469  elnnnn0  11788  nn0sub  11795  zrevaddcl  11876  znnsub  11877  znn0sub  11878  prime  11912  eluz2  12099  indstr  12165  eluz2b1  12168  qrevaddcl  12220  rpneg  12271  xrleltne  12388  dfle2  12390  dflt2  12391  supxrleub  12569  infxrgelb  12578  ixxin  12605  iccid  12633  elicopnf  12683  iccsplit  12721  fzsplit2  12782  fzsn  12799  fzpr  12812  uzsplit  12829  preduz  12879  fvinim0ffz  13006  injresinj  13008  om2uzf1oi  13171  lt2sqi  13402  le2sqi  13403  hashsdom  13590  hashf1lem1  13661  fz1isolem  13667  prprrab  13677  ccatlcan  13916  ccatrcan  13917  s3eq3seq  14137  2swrd2eqwrdeq  14151  trclfvcotr  14203  cnpart  14433  limsuplt  14670  rlimresb  14756  mertenslem2  15074  fprod2dlem  15167  sadadd2lem2  15632  saddisjlem  15646  bitsuz  15656  gcddiv  15728  algcvgblem  15750  isprm3  15856  isprm5  15880  prmreclem5  16085  vdwapun  16139  vdwmc2  16144  ramcl  16194  pwsle  16594  ismre  16690  mreacs  16758  acsfn  16759  iscatd2  16781  cidpropd  16809  dfiso2  16871  oppcsect2  16878  isfunc  16963  setcinv  17179  lubeldm  17420  lubval  17423  glbeldm  17433  glbval  17436  tosso  17475  ipodrsfi  17602  acsfiindd  17616  imasmnd2  17766  submacs  17804  imasgrp2  17971  issubg  18033  resgrpisgrp  18054  subgacs  18068  eqgval  18082  gaorber  18179  symgfix2  18275  psgnran  18374  isslw  18463  sylow2alem2  18473  sylow2a  18474  sylow3lem6  18487  efgcpbllemb  18608  prmcyg  18735  gsum2d2lem  18813  gsumcom2  18815  subgdmdprd  18873  dprd2d2  18883  pgpfac1lem2  18914  pgpfac1lem4  18917  imasring  19059  drngmulne0  19214  subrgacs  19269  sdrgacs  19270  lssle0  19411  lssacs  19429  lssats2  19462  lvecvsn0  19571  islpir  19711  isnzr2  19725  zndvds  20378  znleval  20383  znleval2  20384  lindsmm  20654  islinds3  20660  islindf4  20664  eltg2b  21251  discld  21381  opnssneib  21407  cldlp  21442  restbas  21450  leordtvallem1  21502  leordtvallem2  21503  ssidcn  21547  cnprest2  21582  lmss  21590  perfcls  21657  cmpfi  21700  1stccnp  21754  subislly  21773  hausmapdom  21792  locfindis  21822  iskgen3  21841  kgencn  21848  ptpjpre1  21863  xkoccn  21911  txrest  21923  txlm  21940  txkgen  21944  xkopt  21947  xkoinjcn  21979  imasnopn  21982  imasncld  21983  imasncls  21984  qtopcn  22006  kqfeq  22016  isr0  22029  fbfinnfr  22133  trfbas  22136  fbunfip  22161  ufileu  22211  cfinufil  22220  fmid  22252  txflf  22298  fclsrest  22316  alexsubALT  22343  tsmsres  22435  ucnima  22573  fmucndlem  22583  bldisj  22691  xmeter  22726  elbl4  22856  restmetu  22863  dscopn  22866  bl2ioo  23083  isphtpc  23281  tcphcph  23523  lmmbr2  23545  lmmbrf  23548  iscau2  23563  iscauf  23566  caucfil  23569  metcld  23592  metcld2  23593  bcthlem1  23610  bcthlem4  23613  cldcss2  23728  ovolgelb  23764  ovoliunlem1  23786  ismbfcn  23913  mbfmax  23933  mbfimaopnlem  23939  i1faddlem  23977  i1fmullem  23978  i1fres  23989  i1fpos  23990  itg1climres  23998  xrge0f  24015  itgresr  24062  iblcnlem1  24071  limcun  24176  dvres  24192  mdegmullem  24355  ply1remlem  24439  plyremlem  24576  vieta1  24584  ulmcau  24666  sineq0  24792  coseq1  24793  ang180lem3  25070  cubic  25108  atandm  25135  atandm2  25136  atandm3  25137  rlimcnp  25225  rlimcnp2  25226  vmappw  25375  dchrelbas3  25496  dchrelbas4  25501  dchrsum2  25526  bposlem6  25547  2sqreuopltb  25723  2sqreuopnnltb  25725  dchrisumlem3  25749  pntleml  25869  istrkg3ld  25929  tgcgr4  25999  lnrot2  26092  islnopp  26207  islmib  26255  brbtwn2  26374  axsegconlem6  26391  axsegcon  26396  ax5seg  26407  axpasch  26410  axeuclid  26432  axcontlem4  26436  elntg2  26454  issubgr  26736  nb3gr2nb  26849  uhgrvd00  26999  isrusgr0  27031  wlkcpr  27093  wlkcomp  27095  upgr2wlk  27132  upgrf1istrl  27172  clwlkcomp  27247  clwlkcompbp  27250  iswwlksnx  27305  wspthsnwspthsnon  27382  wspniunwspnon  27389  2pthon3v  27409  usgr2wspthons3  27430  usgr2wspthon  27431  rusgrnumwwlks  27440  clwlkclwwlklem3  27466  clwlkclwwlk  27467  0pth  27591  eupth2lem2  27686  vdgn1frgrv2  27767  fusgreg2wsp  27807  clwwlknonclwlknonf1o  27833  dlwwlknondlwlknonf1o  27836  wlkl0  27838  nmoolb  28239  nmlno0lem  28261  ubthlem1  28338  ocsh  28751  shle0  28910  eigrei  29302  adjeu  29357  nmoplb  29375  nmfnlb  29392  eleigvec2  29426  nmlnop0iALT  29463  cnlnadjlem5  29539  adjbdln  29551  jplem2  29737  cvbr2  29751  mdsl2bi  29791  chrelat3  29839  sq2reunnltb  29940  rmounid  29951  eqsnd  29978  nelpr  29980  disjunsn  30034  ofpreima  30100  funcnvmpt  30102  funcnv5mpt  30103  dfcnv2  30112  gtiso  30124  fpwrelmap  30157  infxrge0glb  30177  xrdifh  30191  fzsplit3  30203  toslublem  30328  tosglblem  30330  isarchi  30449  xrge0tsmsbi  30504  cntzun  30506  smatrcl  30676  unitdivcld  30761  lmxrge0  30812  isrrext  30858  issibf  31208  eulerpartlemr  31249  eulerpartlemmf  31250  eulerpartlemn  31256  dstfrvunirn  31349  ballotlemfc0  31367  ballotlemfcc  31368  reprsuc  31503  reprpmtf1o  31514  reprdifc  31515  bnj919  31655  bnj976  31666  bnj1542  31745  bnj150  31764  bnj151  31765  bnj607  31804  bnj852  31809  bnj873  31812  bnj938  31825  bnj1171  31886  bnj1388  31919  bnj1489  31942  usgrgt2cycl  31986  subfacp1lem3  32038  subfacp1lem5  32040  erdszelem9  32055  kur14  32072  iscvm  32115  satf0op  32233  mclsax  32425  dfpo2  32600  elintfv  32616  fundmpss  32618  opelco3  32627  dfon2  32646  noetalem3  32829  dfbigcup2  32970  sscoid  32984  funpartfv  33016  dfrdg4  33022  cgr3permute3  33118  segletr  33185  segleantisym  33186  seglelin  33187  fneval  33310  neibastop3  33320  eltail  33332  filnetlem4  33339  bj-hbntbi  33640  bj-sbceqgALT  33794  bj-rest10  33997  bj-0int  34011  topdifinffinlem  34178  isbasisrelowllem1  34186  isbasisrelowllem2  34187  rdgeqoa  34201  finxpreclem4  34225  finxpsuclem  34228  uncf  34421  phpreu  34426  cos2h  34433  tan2h  34434  matunitlindflem1  34438  poimirlem16  34458  poimirlem19  34461  poimirlem23  34465  poimirlem24  34466  poimirlem26  34468  poimirlem27  34469  mbfposadd  34489  cnambfre  34490  itg2addnclem  34493  itg2addnc  34496  iblabsnclem  34505  ftc1anclem1  34517  ftc1anclem5  34521  caures  34586  heiborlem3  34642  heiborlem10  34649  elghomOLD  34716  divrngidl  34857  eqrelf  35068  brvbrvvdif  35076  eldmqsres2  35095  exanres  35103  ssrel3  35107  relcnveq  35130  iss2  35152  ecinn0  35158  brxrn2  35177  ecxrn  35189  eldmcoss2  35249  eldm1cossres  35250  elrelsrel  35277  elrelscnveq  35282  elcoeleqvrelsrel  35381  brredundsredund  35412  brdmqssqs  35432  cnvepresdmqss  35436  eldmqs1cossres  35443  brerser  35460  erim2  35461  eleldisjseldisj  35512  prtlem10  35551  prtlem16  35555  prtlem19  35564  prtex  35566  prter3  35568  islshpat  35703  lcvbr2  35708  lcvbr3  35709  lshpsmreu  35795  isat3  35993  hlrelat5N  36087  islpln5  36221  cdlemblem  36479  paddvaln0N  36487  paddval0  36496  cdlemefrs29bpre1  37083  cdlemefrs29cpre1  37084  cdlemg27b  37382  cdlemg33c  37394  cdlemg33e  37396  diaglbN  37741  cdlemm10N  37804  dicopelval2  37867  dicelval2N  37868  dihopelvalcpre  37934  dihglbcpreN  37986  dih1dimatlem  38015  dihatexv  38024  dvh4dimlem  38129  mapdpglem3  38361  hdmap14lem13  38566  hdmapglem7a  38613  fnsnbt  38669  isnacs2  38807  rabrenfdioph  38915  expdiophlem1  39122  pw2f1ocnv  39138  pwfi2f1o  39200  numinfctb  39207  dfacbasgrp  39212  islnr3  39219  isdomn3  39308  dfhe3  39625  clsk3nimkb  39894  ntrneiiso  39945  ntrneikb  39948  scottabf  40092  mnuunid  40129  hashnzfzclim  40211  dvconstbi  40223  sbcoreleleqVD  40751  rfcnpre3  40848  rfcnpre4  40849  unima  40981  cncfshift  41718  stoweidlem59  41906  dfafv23  42988  nelbrnel  43011  iccpartiun  43096  prproropf1olem0  43166  prprelb  43180  prprspr2  43182  reuprpr  43187  oddm1evenALTV  43342  oddp1evenALTV  43343  oddprmne2  43382  fpprel  43395  submgmacs  43573  ismhm0  43574  iscmgmALT  43629  iscsgrpALT  43631  isrnghmmul  43662  elpglem2  44314