Theorem syl5bb 272

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

Hypotheses

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

Assertion

Ref	Expression
syl5bb	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem syl5bb

Step	Hyp	Ref	Expression
1		syl5bb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3		syl5bb.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 268	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  syl5rbb  273  syl5bbr  274  3bitr4g  303  imim21b  382  ifpfal  1024  cad0  1556  ax12wdemo  2012  sbal2  2461  necon3abid  2830  necon3bid  2838  ralxpxfr2d  3327  ceqsrexv  3336  ceqsrex2v  3338  elab2g  3353  elrabf  3360  elrab3t  3362  eueq2  3380  eqreu  3398  reu8  3402  ru  3434  sbcralt  3510  sbcabel  3517  sbcel1g  3987  sbcel2  3989  csbnestgf  3996  sbccsb2  4005  disjpss  4028  sbcssg  4085  rexsng  4219  ralprg  4234  rexprg  4235  difsn  4328  preq2b  4378  opthpr  4384  preqsnd  4392  csbopg  4420  ralunsn  4422  csbuni  4466  dfiin2g  4553  iunxsng  4602  elpwuni  4616  disjxun  4651  sbcbr12g  4708  pwnss  4830  opthneg  4950  otthg  4954  opelopabt  4987  opelopabga  4988  brabga  4989  opelopabgf  4995  csbmpt12  5010  rbropapd  5015  dfid3  5025  frirr  5091  wereu2  5111  opeliunxp  5170  posn  5187  sosn  5188  frsn  5189  brab2a  5194  opbrop  5198  csbcnvgALT  5307  elrnmpt1  5374  elrnmptg  5375  eliniseg2  5505  poleloe  5527  xpdifid  5562  cnvpo  5673  elpred  5693  ordtri4  5761  oneqmini  5776  elsucg  5792  elsuc2g  5793  sbcfung  5912  dffun8  5916  fncnv  5962  fununi  5964  fnssresb  6003  fnimaeq0  6013  csbfv12  6231  dffn5  6241  funimass4  6247  feqmptdf  6251  fnsnfv  6258  dmfco  6272  fndmdif  6321  fvimacnvi  6331  fvimacnvALT  6336  unpreima  6341  respreima  6344  fmptco  6396  fressnfv  6427  fmptsnd  6435  fnnfpeq0  6444  tpres  6466  elunirn  6509  dff13  6512  f12dfv  6529  f13dfv  6530  fliftel  6559  isoini  6588  f1oiso  6601  riotaeqimp  6634  eloprabga  6747  resoprab2  6757  elrnmpt2res  6774  ralrnmpt2  6775  ovid  6777  ov  6780  ovg  6799  ofrfval2  6915  dfwe2  6981  ssonprc  6992  ordpwsuc  7015  dfom2  7067  f1oweALT  7152  el2xptp0  7212  fmpt2x  7236  ovmptss  7258  1stconst  7265  2ndconst  7266  fnsuppres  7322  brtpos2  7358  mpt2curryd  7395  dfsmo2  7444  rdglim2  7528  seqomlem2  7546  omeu  7665  oeeui  7682  brdifun  7771  eqerlem  7776  brecop  7840  erovlem  7843  eceqoveq  7853  mapsn  7899  ixpsnval  7911  mptelixpg  7945  map1  8036  xpsnen  8044  xpdom2  8055  omxpenlem  8061  xpf1o  8122  mapunen  8129  onfin  8151  fimaxg  8207  fodomfib  8240  fofinf1o  8241  fipreima  8272  supub  8365  infglb  8396  infglbb  8397  fiming  8404  fiinfg  8405  ordtypecbv  8422  ordtypelem3  8425  ordtypelem9  8431  hartogslem1  8447  wofib  8450  wemapsolem  8455  wemapso2lem  8457  noinfep  8557  cantnf  8590  rankbnd2  8732  domtri2  8815  infxpenc2  8845  fseqdom  8849  acni2  8869  dfac9  8958  cfeq0  9078  cfsuc  9079  cflim3  9084  cfslb  9088  cofsmo  9091  enfin2i  9143  isfin3ds  9151  isf33lem  9188  fin1a2lem5  9226  axdc2lem  9270  zorn2g  9325  fodomb  9348  brdom7disj  9353  brdom6disj  9354  iundom2g  9362  cfpwsdom  9406  elgch  9444  fpwwe2cbv  9452  fpwwecbv  9466  pwfseqlem3  9482  pwfseqlem4a  9483  pwfseqlem4  9484  ltpiord  9709  nlt1pi  9728  nqereu  9751  addclprlem1  9838  1idpr  9851  reclem3pr  9871  ltsosr  9915  map2psrpr  9931  supsrlem  9932  axrrecex  9984  xrlenlt  10103  eqlei2  10148  addsubeq4  10296  renegcli  10342  lesub0  10545  wloglei  10560  conjmul  10742  rereccl  10743  infm3  10982  supaddc  10990  supadd  10991  supmul1  10992  supmullem1  10993  supmullem2  10994  supmul  10995  creui  11015  nndiv  11061  elznn0  11392  prime  11458  eqreznegel  11774  zsupss  11777  rebtwnz  11787  negelrp  11864  ltxr  11949  elixx3g  12188  ixxun  12191  ioo0  12200  ico0  12221  ioc0  12222  icc0  12223  difreicc  12304  divelunit  12314  iccf1o  12316  elfz2  12333  fzn  12357  fznn  12408  fzshftral  12428  nelfzo  12475  fzosplitsni  12579  om2uzisoi  12753  rabssnn0fi  12785  mptnn0fsupp  12797  sq11i  12954  hashsdom  13170  fi1uzind  13279  fi1uzindOLD  13285  wrdval  13308  csbwrdg  13334  wrd2ind  13477  s2f1o  13661  cjreb  13863  rexfiuz  14087  cau3lem  14094  rlim2  14227  ello12  14247  ello1mpt  14252  elo12  14258  o1lo1  14268  lo1resb  14295  o1resb  14297  o1compt  14318  caucvgb  14410  pwm1geoser  14600  mertens  14618  ruclem12  14970  divides  14985  dvdsabseq  15035  odd2np1  15065  oddm1even  15067  sumodd  15111  divalgmod  15129  modremain  15132  sadadd2lem2  15172  gcdcllem2  15222  bezoutlem2  15257  bezoutlem3  15258  bezoutlem4  15259  isprm2  15395  isprm3  15396  dvdsnprmd  15403  oddprmdvds  15607  prmreclem2  15621  prmreclem5  15624  prmreclem6  15625  4sqlem2  15653  4sqlem12  15660  vdwmc  15682  vdwpc  15684  vdwlem6  15690  vdwlem10  15694  vdwnn  15702  ramval  15712  0ram  15724  prdsleval  16137  pwsle  16152  imasleval  16201  xpsfrnel2  16225  xpsle  16241  isacs2  16314  mreacs  16319  acsfn  16320  iscatd2  16342  catpropd  16369  ciclcl  16462  cicrcl  16463  isssc  16480  evlfcl  16862  uncfcurf  16879  pltval  16960  lublecllem  16988  tosso  17036  oduleg  17132  oduclatb  17144  posglbmo  17147  isipodrs  17161  odudlatb  17196  gsumvalx  17270  sgrp2rid2  17413  grplmulf1o  17489  grplactcnv  17518  elnmz  17633  eqgid  17646  isghm  17660  ghmeqker  17687  resscntz  17764  symg1bas  17816  pgrpsubgsymgbi  17827  symgfixelq  17853  f1omvdconj  17866  odmulgeq  17974  sylow3lem3  18044  sylow3lem6  18047  efgval2  18137  efgsdm  18143  efgrelexlema  18162  efgcpbllemb  18168  iscyggen2  18283  cyggenod  18286  gsummptfzcl  18368  eldprd  18403  dprdf11  18422  dprddisj2  18438  pgpfac1lem2  18474  pgpfac1  18479  srg1zr  18529  drngid2  18763  issubrg  18780  islmod  18867  aspval2  19347  psrbag  19364  cply1coe0bi  19670  zndvds  19898  znleval  19903  iunocv  20025  pjfval2  20053  pjdm2  20055  dsmmelbas  20083  ellspd  20141  islindf  20151  islindf4  20177  istopg  20700  basgen2  20793  isclo  20891  mretopd  20896  isnei  20907  isperf3  20957  restdis  20982  neitr  20984  restcls  20985  restlp  20987  restperf  20988  iscn  21039  iscnp  21041  lmbr2  21063  lmbrf  21064  ordtt1  21183  cmpsub  21203  hauscmplem  21209  cmpfi  21211  dfconn2  21222  1stcelcls  21264  1stccn  21266  nllyi  21278  subislly  21284  dissnlocfin  21332  elkgen  21339  ptpjpre1  21374  ptuni2  21379  ptclsg  21418  ptcnplem  21424  txcn  21429  hausdiag  21448  txhaus  21450  txkgen  21455  xkoptsub  21457  cnmpt21  21474  elqtop  21500  tgqtop  21515  r0cld  21541  elfg  21675  fbasrn  21688  trfil2  21691  trfil3  21692  fin1aufil  21736  elfm2  21752  elfm3  21754  flimopn  21779  fbflim  21780  flfnei  21795  flftg  21800  cnpflf2  21804  txflf  21810  fclsbas  21825  alexsubALTlem4  21854  cnextfvval  21869  snclseqg  21919  tgphaus  21920  tsmsfbas  21931  tsmssubm  21946  utopsnneip  22052  prdsxmetlem  22173  imasdsf1olem  22178  xpsdsval  22186  blres  22236  isxms2  22253  metcnp  22346  txmetcnp  22352  txmetcn  22353  metustel  22355  metuel2  22370  dscopn  22378  isngp4  22416  cnblcld  22578  metnrmlem1a  22661  icoopnst  22738  iocopnst  22739  elpi1  22845  isclmp  22897  isncvsngp  22949  lmmbr2  23057  cfil3i  23067  caucfil  23081  iscmet3  23091  lmclim  23101  metcld2  23105  bcthlem4  23124  minveclem3b  23199  minveclem6  23205  minveclem7  23206  ivthle  23225  ivthle2  23226  evthicc2  23229  ovolfioo  23236  ovolficc  23237  ovolgelb  23248  dyadmax  23366  subopnmbl  23372  ismbf3d  23421  mbfimaopnlem  23422  mbfimaopn2  23424  mbfaddlem  23427  mbfsup  23431  mbfinf  23432  i1f1lem  23456  i1fmulclem  23469  itg1climres  23481  mbfi1fseqlem4  23485  itg2monolem1  23517  itg2gt0  23527  isibl  23532  iblcnlem1  23554  ellimc2  23641  dvcnvrelem1  23780  itgsubst  23812  mdegleb  23824  fta1glem2  23926  quotval  24047  vieta1lem1  24065  vieta1lem2  24066  ulm2  24139  ulmcaulem  24148  ulmcau  24149  radcnvlt1  24172  sineq0  24273  cos11  24279  recosf1o  24281  efopn  24404  cxpeq  24498  mcubic  24574  birthdaylem3  24680  rlimcnp  24692  xrlimcnp  24695  eldmgm  24748  dmgmaddn0  24749  lgamgulmlem6  24760  wilth  24797  isppw  24840  isppw2  24841  mumullem2  24906  sqff1o  24908  dvdsmulf1o  24920  fsumvma  24938  fsumvma2  24939  vmasum  24941  chpchtsum  24944  lgsne0  25060  gausslemma2dlem0i  25089  gausslemma2dlem1a  25090  lgseisenlem2  25101  lgsquadlem1  25105  lgsquadlem2  25106  2lgslem1a  25116  dchrmusumlema  25182  rpvmasum2  25201  dchrisum0lema  25203  pntibndlem3  25281  pntlemi  25293  pntleml  25300  pnt3  25301  trgcgrg  25410  tgcgr4  25426  colcom  25453  colrot1  25454  ltgov  25492  hlcomb  25498  lncom  25517  mirreu3  25549  isperp  25607  perpcom  25608  brbtwn  25779  brcgr  25780  brbtwn2  25785  colinearalg  25790  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  edgiedgb  25947  isuhgr  25955  isushgr  25956  isupgr  25979  isumgr  25990  isuspgr  26047  isusgr  26048  uhgr0v0e  26130  isfusgrf1  26212  opfusgr  26215  usgr1v0e  26218  dfnbgr3  26236  nbuhgr2vtx1edgb  26248  edgnbusgreu  26269  nbusgredgeu0  26270  isuvtxa  26295  cusgruvtxb  26318  cplgr3v  26331  cusgrsizeinds  26348  vtxdg0v  26369  vtxd0nedgb  26384  vtxduhgr0nedg  26388  vtxdusgr0edgnelALT  26392  iswlk  26506  wlk1walk  26535  upgr2wlk  26564  upgristrl  26599  2pthnloop  26627  usgr2pthlem  26659  isclwlke  26673  isclwlkupgr  26674  iswwlksnx  26731  wwlksnextwrd  26792  wwlksnextproplem3  26806  2pthon3v  26839  umgr2wlk  26845  elwwlks2  26861  elwspths2spth  26862  clwlkclwwlk  26903  clwwlksn2  26910  eclclwwlksn1  26952  eleclclwwlksn  26953  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfclwwlk1hashn  26959  clwlksfoclwwlk  26963  clwwlksnun  26974  1pthon2v  27013  uhgr3cyclex  27042  isconngr  27049  isconngr1  27050  eupthres  27075  eupth2lems  27098  isfrgr  27122  frgr0v  27125  frgr3vlem2  27138  fusgr2wsp2nb  27198  isvclem  27432  isnvlem  27465  isphg  27672  isph  27677  phoeqi  27713  ubthlem3  27728  minvecolem5  27737  minvecolem6  27738  minvecolem7  27739  hhph  28035  issh3  28076  nmopub  28767  nmfnleub  28784  adjeq  28794  adjvalval  28796  elunop2  28872  lnophm  28878  nmcexi  28885  cnlnadjlem5  28930  cnlnadjeui  28936  adjbd1o  28944  jpi  29129  mddmd2  29168  chrelati  29223  chrelat2i  29224  cvexchlem  29227  dmdbr5ati  29281  cdjreui  29291  cdj3i  29300  iunxsngf  29375  disjunsn  29407  opeldifid  29412  fcoinvbr  29419  brabgaf  29420  opabdm  29423  opabrn  29424  iunsnima  29428  elimampt  29438  abfmpunirn  29452  fmptcof2  29457  funcnvmptOLD  29467  funcnvmpt  29468  funcnv5mpt  29469  f1od2  29499  resf1o  29505  fpwrelmap  29508  iocinioc2  29541  eliccioo  29639  posrasymb  29657  isslmd  29755  smatrcl  29862  pstmxmet  29940  prsdm  29960  prsrn  29961  ordtconnlem1  29970  xrmulc1cn  29976  ispisys2  30216  elcarsg  30367  eulerpartlemmf  30437  isrrvv  30505  reprinrn  30696  tgoldbachgt  30741  bnj976  30848  bnj944  31008  bnj1173  31070  bnj1321  31095  bnj1373  31098  bnj1417  31109  subfacp1lem3  31164  subfacp1lem6  31167  subfacp1  31168  txpconn  31214  sconnpi1  31221  resconn  31228  cvmscbv  31240  cvmsval  31248  cvmlift2lem13  31297  cvmlift3lem2  31302  cvmlift3  31310  mclsrcl  31458  br8  31646  br6  31647  br4  31648  elintfv  31662  fv1stcnv  31680  fv2ndcnv  31681  distel  31709  poseq  31750  wsuclem  31773  wsuclemOLD  31774  sltsolem1  31826  nosupdm  31850  nosupbnd1lem4  31857  slenlt  31877  sleloe  31879  etasslt  31920  madeval2  31936  imageval  32037  funpartfv  32052  dfrdg4  32058  altopthg  32074  altopthbg  32075  brcolinear2  32165  lineext  32183  brsegle  32215  seglelin  32223  broutsideof2  32229  isfne4  32335  isfne2  32337  isfne3  32338  fneval  32347  topfneec  32350  neibastop2lem  32355  neibastop2  32356  neifg  32366  filnetlem4  32376  onsuct0  32440  bj-abbi  32775  bj-tagcg  32973  bj-projval  32984  bj-restuni  33050  bj-raldifsn  33054  csbwrecsg  33173  csboprabg  33176  csbmpt22g  33177  topdifinffinlem  33195  isbasisrelowllem1  33203  isbasisrelowllem2  33204  rdgeqoa  33218  csbfinxpg  33225  wl-sbrimt  33331  wl-sblimt  33332  wl-sbnf1  33336  wl-mo2df  33352  wl-eudf  33354  wl-mo2t  33357  wl-mo3t  33358  wl-ax11-lem6  33367  uncov  33390  tan2h  33401  matunitlindf  33407  ptrest  33408  poimirlem2  33411  poimirlem16  33425  poimirlem19  33428  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  mbfposadd  33457  cnambfre  33458  itg2addnclem2  33462  fdc  33541  heibor1  33609  rrncmslem  33631  rrnheibor  33636  opidonOLD  33651  issmgrpOLD  33662  ismndo  33671  isrngo  33696  isdivrngo  33749  isfldidl2  33868  isdmn3  33873  releleccnv  34021  releccnveq  34022  brcnvep  34029  opelresALTV  34031  elecres  34042  eleccnvep  34046  ideq2  34078  extid  34081  relcnveq3  34092  eqres  34108  opideq  34110  ecin0  34117  alrmomo2  34124  prtlem13  34153  prter3  34167  lrelat  34301  islshpat  34304  lshpsmreu  34396  lkrpssN  34450  cmtvalN  34498  omllaw2N  34531  cvrval  34556  cvrval2  34561  cvlsupr3  34631  3dim0  34743  islln2  34797  islpln5  34821  islpln2  34822  islpln2ah  34835  islvol5  34865  islvol2  34866  4atlem11  34895  pmapglbx  35055  cdleme18d  35582  cdlemefrs29bpre0  35684  cdlemb3  35894  cdlemg33b  35995  cdlemkid3N  36221  cdlemkid4  36222  dvhb1dimN  36274  dia11N  36337  cdlemm10N  36407  dib11N  36449  dib1dim  36454  dibglbN  36455  diblsmopel  36460  dihopelvalcpre  36537  dih11  36554  dihmeetlem4preN  36595  dihmeetlem13N  36608  lcfrvalsnN  36830  lcfrlem9  36839  lcf1o  36840  mapdval4N  36921  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  hdmap1fval  37086  hdmapfval  37119  hdmapglem7a  37219  hlhillcs  37250  ellz1  37330  lzunuz  37331  fz1eqin  37332  diophrex  37339  rexrabdioph  37358  rexfrabdioph  37359  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  fzneg  37549  expdioph  37590  wepwsolem  37612  fnwe2lem2  37621  islmodfg  37639  kercvrlsm  37653  sdrgacs  37771  cnvcnvintabd  37906  iunrelexpuztr  38011  brtrclfv2  38019  frege124d  38053  rcompleq  38318  or3or  38319  uneqsn  38321  clsk1independent  38344  ntrclsneine0lem  38362  ntrclsiso  38365  ntrclsk2  38366  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  ntrclsk4  38370  ntrneiel2  38384  ntrneiiso  38389  ntrneikb  38392  ntrneik3  38394  ntrneix3  38395  ntrneik13  38396  ntrneix13  38397  ntrneik4w  38398  k0004lem3  38447  pm10.52  38564  iotasbc  38620  pm14.122a  38623  pm14.122b  38624  pm14.123a  38626  rusbcALT  38640  fvsb  38656  trsbc  38750  rexsngf  39220  iunxsngf2  39230  mapsnd  39388  limcperiod  39860  limsupre  39873  dvbdfbdioo  40145  stoweidlem34  40251  fourierdlem108  40431  fourierdlem110  40433  etransc  40500  2reu4a  41189  funressnfv  41208  dfafn5a  41240  elfz2z  41325  el1fzopredsuc  41335  iccelpart  41369  lighneallem2  41523  dfeven2  41562  gbowge7  41651  sbgoldbwt  41665  isupwlk  41717  uspgrsprfo  41756  ismhm0  41805  inclfusubc  41867  isrnghm  41892  rnghmval2  41895  uzlidlring  41929  lidldomnnring  41930  zrninitoringc  42071  opeliun2xp  42111  snlindsntor  42260  elbigo2  42346  gte-lte  42465  gt-lt  42466