Theorem syl5bb 286

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 282	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  syl5rbb  287  bitr3id  288  3bitr4g  317  imim21b  398  ifpfal  1072  norass  1534  cad0  1619  ax12wdemo  2136  eu6lem  2633  abbi  2865  necon3abid  3023  necon3bid  3031  ralxpxfr2d  3587  ceqsrexv  3597  ceqsrex2v  3599  elab2gw  3613  elab2g  3616  elrabf  3624  elrab3t  3627  eueq2  3649  eqreu  3668  reu8  3672  ru  3719  sbcralt  3801  sbcabel  3807  ss2abdv  3991  rcompleq  4220  sbcel1g  4321  sbcel2  4323  csbnestgfw  4327  csbnestgf  4332  sbccsb2  4342  2nreu  4349  disjpss  4368  sbcssg  4421  2reu4lem  4423  rexsngf  4570  reusngf  4572  ralprgf  4590  rexprgf  4591  reuprg0  4598  difsn  4691  preq2b  4738  opthpr  4742  preqsnd  4749  csbopg  4783  ralunsn  4786  csbuni  4829  dfiin2g  4919  iunxsng  4975  iunxsngf  4977  elpwuni  4990  disjxun  5028  sbcbr12g  5086  opthneg  5338  otthg  5342  opeqsng  5358  snopeqop  5361  opelopabt  5384  opelopabga  5385  brabga  5386  opelopabgf  5392  csbmpt12  5409  rbropapd  5414  dfid3  5427  frirr  5496  wereu2  5516  opeliunxp  5583  posn  5601  sosn  5602  frsn  5603  brab2a  5608  opbrop  5612  csbcnvgALT  5719  dmopabelb  5749  elrnmpt1  5794  elrnmptg  5795  opelres  5824  eliniseg2  5936  poleloe  5958  xpdifid  5992  cnvpo  6106  reu3op  6111  elpred  6129  ordtri4  6196  oneqmini  6210  elsucg  6226  elsuc2g  6227  sbcfung  6348  dffun8  6352  fncnv  6397  fununi  6399  fnssresb  6441  fnimaeq0  6453  csbfv12  6688  dffn5  6699  funimass4  6705  feqmptdf  6710  fnsnfv  6718  dmfco  6734  fndmdif  6789  fvimacnvi  6799  fvimacnvALT  6804  unpreima  6810  respreima  6813  fmptco  6868  fressnfv  6899  fmptsnd  6908  fnnfpeq0  6917  tpres  6940  elunirn  6988  dff13  6991  f12dfv  7008  f13dfv  7009  fliftel  7041  isoini  7070  f1oiso  7083  riotaeqimp  7119  fnbrovb  7184  eloprabga  7240  resoprab2  7250  elrnmpores  7267  ralrnmpo  7268  ovid  7270  ov  7273  ovg  7293  ofrfval2  7407  dfwe2  7476  ssonprc  7487  ordpwsuc  7510  dfom2  7562  f1oweALT  7655  el2xptp0  7718  releldmdifi  7726  fmpox  7747  ovmptss  7771  1stconst  7778  2ndconst  7779  fnsuppres  7840  suppcoss  7854  brtpos2  7881  mpocurryd  7918  dfsmo2  7967  rdglim2  8051  seqomlem2  8070  omeu  8194  oeeui  8211  brdifun  8301  eqerlem  8306  brecop  8373  erovlem  8376  eceqoveq  8385  mapsnd  8433  ixpsnval  8447  mptelixpg  8482  xpsnen  8584  xpdom2  8595  omxpenlem  8601  xpf1o  8663  mapunen  8670  onfin  8694  fimaxg  8749  fodomfib  8782  fofinf1o  8783  fipreima  8814  supub  8907  infglb  8938  infglbb  8939  fiming  8946  fiinfg  8947  ordtypecbv  8965  ordtypelem3  8968  ordtypelem9  8974  hartogslem1  8990  wofib  8993  wemapsolem  8998  wemapso2lem  9000  noinfep  9107  cantnf  9140  rankbnd2  9282  domtri2  9402  infxpenc2  9433  fseqdom  9437  acni2  9457  dfac9  9547  cfeq0  9667  cfsuc  9668  cflim3  9673  cfslb  9677  cofsmo  9680  enfin2i  9732  isfin3ds  9740  isf33lem  9777  fin1a2lem5  9815  axdc2lem  9859  zorn2g  9914  fodomb  9937  brdom7disj  9942  brdom6disj  9943  iundom2g  9951  cfpwsdom  9995  elgch  10033  fpwwe2cbv  10041  fpwwecbv  10055  pwfseqlem3  10071  pwfseqlem4a  10072  pwfseqlem4  10073  ltpiord  10298  nlt1pi  10317  nqereu  10340  addclprlem1  10427  1idpr  10440  reclem3pr  10460  ltsosr  10505  map2psrpr  10521  supsrlem  10522  axrrecex  10574  xrlenlt  10695  eqlei2  10740  addsubeq4  10890  renegcli  10936  lesub0  11146  wloglei  11161  conjmul  11346  rereccl  11347  infm3  11587  supaddc  11595  supadd  11596  supmul1  11597  supmullem1  11598  supmullem2  11599  supmul  11600  creui  11620  nndiv  11671  elznn0  11984  prime  12051  eqreznegel  12322  zsupss  12325  rebtwnz  12335  negelrp  12410  ltxr  12498  elixx3g  12739  ixxun  12742  ioo0  12751  ico0  12772  ioc0  12773  icc0  12774  difreicc  12862  divelunit  12872  iccf1o  12874  elfz2  12892  fzn  12918  fznn  12970  fzshftral  12990  nelfzo  13038  fzosplitsni  13143  om2uzisoi  13317  rabssnn0fi  13349  mptnn0fsupp  13360  sq11i  13550  hashsdom  13738  fi1uzind  13851  wrdval  13860  csbwrdg  13887  wrd2ind  14076  s2f1o  14269  cjreb  14474  rexfiuz  14699  cau3lem  14706  rlim2  14845  ello12  14865  ello1mpt  14870  elo12  14876  o1lo1  14886  lo1resb  14913  o1resb  14915  o1compt  14936  caucvgb  15028  pwm1geoserOLD  15217  mertens  15234  ruclem12  15586  divides  15601  dvdsabseq  15655  odd2np1  15682  oddm1even  15684  sumodd  15729  divalgmod  15747  modremain  15749  sadadd2lem2  15789  gcdcllem2  15839  bezoutlem2  15878  bezoutlem3  15879  bezoutlem4  15880  isprm2  16016  isprm3  16017  dvdsnprmd  16024  oddprmdvds  16229  prmreclem2  16243  prmreclem5  16246  prmreclem6  16247  4sqlem2  16275  4sqlem12  16282  vdwmc  16304  vdwpc  16306  vdwlem6  16312  vdwlem10  16316  vdwnn  16324  ramval  16334  0ram  16346  prdsleval  16742  pwsle  16757  imasleval  16806  xpsfrnel2  16829  xpsle  16844  isacs2  16916  mreacs  16921  acsfn  16922  iscatd2  16944  catpropd  16971  ciclcl  17064  cicrcl  17065  isssc  17082  evlfcl  17464  uncfcurf  17481  pltval  17562  lublecllem  17590  tosso  17638  oduleg  17734  oduclatb  17746  posglbmo  17749  isipodrs  17763  odudlatb  17798  gsumvalx  17878  elefmndbas  18030  sgrp2rid2  18083  grplmulf1o  18165  grplactcnv  18194  elnmz  18307  eqgid  18324  isghm  18350  ghmeqker  18377  resscntz  18454  symg1bas  18511  pgrpsubgsymgbi  18528  symgfixelq  18553  f1omvdconj  18566  odmulgeq  18676  sylow3lem3  18746  sylow3lem6  18749  efgval2  18842  efgsdm  18848  efgrelexlema  18867  efgcpbllemb  18873  iscyggen2  18993  cyggenod  18996  gsummptfzcl  19082  eldprd  19119  dprdf11  19138  dprddisj2  19154  pgpfac1lem2  19190  pgpfac1  19195  srg1zr  19272  drngid2  19511  issubrg  19528  sdrgacs  19573  islmod  19631  zndvds  20241  znleval  20246  iunocv  20370  pjfval2  20398  pjdm2  20400  dsmmelbas  20428  ellspd  20491  islindf  20501  islindf4  20527  aspval2  20584  psrbag  20602  cply1coe0bi  20929  istopg  21500  basgen2  21594  isclo  21692  mretopd  21697  isnei  21708  isperf3  21758  restdis  21783  neitr  21785  restcls  21786  restlp  21788  restperf  21789  iscn  21840  iscnp  21842  lmbr2  21864  lmbrf  21865  ordtt1  21984  cmpsub  22005  hauscmplem  22011  cmpfi  22013  dfconn2  22024  1stcelcls  22066  1stccn  22068  nllyi  22080  subislly  22086  dissnlocfin  22134  elkgen  22141  ptpjpre1  22176  ptuni2  22181  ptclsg  22220  ptcnplem  22226  txcn  22231  hausdiag  22250  txhaus  22252  txkgen  22257  xkoptsub  22259  cnmpt21  22276  elqtop  22302  tgqtop  22317  r0cld  22343  elfg  22476  fbasrn  22489  trfil2  22492  trfil3  22493  fin1aufil  22537  elfm2  22553  elfm3  22555  flimopn  22580  fbflim  22581  flfnei  22596  flftg  22601  cnpflf2  22605  txflf  22611  fclsbas  22626  alexsubALTlem4  22655  cnextfvval  22670  snclseqg  22721  tgphaus  22722  tsmsfbas  22733  tsmssubm  22748  utopsnneip  22854  prdsxmetlem  22975  imasdsf1olem  22980  xpsdsval  22988  blres  23038  isxms2  23055  metcnp  23148  txmetcnp  23154  txmetcn  23155  metustel  23157  metuel2  23172  dscopn  23180  isngp4  23218  cnblcld  23380  metnrmlem1a  23463  icoopnst  23544  iocopnst  23545  elpi1  23650  isclmp  23702  isncvsngp  23754  lmmbr2  23863  cfil3i  23873  caucfil  23887  iscmet3  23897  lmclim  23907  metcld2  23911  bcthlem4  23931  minveclem3b  24032  minveclem6  24038  minveclem7  24039  ivthle  24060  ivthle2  24061  evthicc2  24064  ovolfioo  24071  ovolficc  24072  ovolgelb  24084  dyadmax  24202  subopnmbl  24208  ismbf3d  24258  mbfimaopnlem  24259  mbfimaopn2  24261  mbfaddlem  24264  mbfsup  24268  mbfinf  24269  i1f1lem  24293  i1fmulclem  24306  itg1climres  24318  mbfi1fseqlem4  24322  itg2monolem1  24354  itg2gt0  24364  isibl  24369  iblcnlem1  24391  ellimc2  24480  dvcnvrelem1  24620  itgsubst  24652  mdegleb  24665  fta1glem2  24767  quotval  24888  vieta1lem1  24906  vieta1lem2  24907  ulm2  24980  ulmcaulem  24989  ulmcau  24990  radcnvlt1  25013  sineq0  25116  cos11  25125  recosf1o  25127  efopn  25249  cxpeq  25346  mcubic  25433  birthdaylem3  25539  rlimcnp  25551  xrlimcnp  25554  eldmgm  25607  dmgmaddn0  25608  lgamgulmlem6  25619  wilth  25656  isppw  25699  isppw2  25700  mumullem2  25765  sqff1o  25767  dvdsmulf1o  25779  fsumvma  25797  fsumvma2  25798  vmasum  25800  chpchtsum  25803  lgsne0  25919  gausslemma2dlem0i  25948  gausslemma2dlem1a  25949  lgseisenlem2  25960  lgsquadlem1  25964  lgsquadlem2  25965  2lgslem1a  25975  addsq2reu  26024  2sqreu  26040  2sqreunn  26041  2sqreult  26042  2sqreunnlt  26044  dchrmusumlema  26077  rpvmasum2  26096  dchrisum0lema  26098  pntibndlem3  26176  pntlemi  26188  pntleml  26195  pnt3  26196  trgcgrg  26309  tgcgr4  26325  colcom  26352  colrot1  26353  ltgov  26391  hlcomb  26397  lncom  26416  mirreu3  26448  isperp  26506  perpcom  26507  iscgra  26603  isinag  26632  brbtwn  26693  brcgr  26694  brbtwn2  26699  colinearalg  26704  axeuclidlem  26756  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  elntg2  26779  edgiedgb  26847  isuhgr  26853  isushgr  26854  isupgr  26877  isumgr  26888  isuspgr  26945  isusgr  26946  uhgr0v0e  27028  isfusgrf1  27110  opfusgr  27113  usgr1v0e  27116  dfnbgr3  27128  nbuhgr2vtx1edgb  27142  edgnbusgreu  27157  nbusgredgeu0  27158  isuvtx  27185  cusgruvtxb  27212  cplgr3v  27225  cusgrsizeinds  27242  vtxdg0v  27263  vtxd0nedgb  27278  vtxduhgr0nedg  27282  vtxdusgr0edgnelALT  27286  iswlk  27400  wlk1walk  27428  upgr2wlk  27458  upgristrl  27492  2pthnloop  27520  usgr2pthlem  27552  isclwlke  27566  isclwlkupgr  27567  iswwlksnx  27626  wwlksnextwrd  27683  wwlksnextproplem3  27697  2pthon3v  27729  umgr2wlk  27735  elwwlks2on  27745  elwwlks2  27752  elwspths2spth  27753  clwwlknclwwlkdif  27764  clwlkclwwlk  27787  clwlkclwwlk2  27788  clwwlkn1  27826  clwwlkn2  27829  clwwlkwwlksb  27839  eclclwwlkn1  27860  eleclclwwlkn  27861  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  clwwlknonel  27880  clwwlknon1  27882  clwwlknun  27897  1pthon2v  27938  uhgr3cyclex  27967  isconngr  27974  isconngr1  27975  eupthres  28000  eupth2lems  28023  frgr0v  28047  frgr3vlem2  28059  fusgr2wsp2nb  28119  extwwlkfab  28137  numclwwlk1lem2foa  28139  numclwwlk1lem2fo  28143  isvclem  28360  isnvlem  28393  isphg  28600  isph  28605  phoeqi  28640  ubthlem3  28655  minvecolem5  28664  minvecolem6  28665  minvecolem7  28666  hhph  28961  issh3  29002  nmopub  29691  nmfnleub  29708  adjeq  29718  adjvalval  29720  elunop2  29796  lnophm  29802  nmcexi  29809  cnlnadjlem5  29854  cnlnadjeui  29860  adjbd1o  29868  jpi  30053  mddmd2  30092  chrelati  30147  chrelat2i  30148  cvexchlem  30151  dmdbr5ati  30205  cdjreui  30215  cdj3i  30224  elunsn  30281  disjunsn  30357  opeldifid  30362  fcoinvbr  30371  brabgaf  30372  opabdm  30375  opabrn  30376  iunsnima  30382  nfpconfp  30391  elimampt  30397  abfmpunirn  30415  fmptcof2  30420  funcnvmpt  30430  funcnv5mpt  30431  suppiniseg  30446  ressupprn  30450  brsnop  30453  brprop  30457  f1od2  30483  resf1o  30492  fpwrelmap  30495  iocinioc2  30528  eliccioo  30633  wrdt2ind  30653  posrasymb  30670  mcgcnv  30705  isslmd  30880  prmidl0  31034  fedgmullem2  31114  smatrcl  31149  rspectopn  31220  pstmxmet  31250  prsdm  31267  prsrn  31268  ordtconnlem1  31277  xrmulc1cn  31283  ispisys2  31522  elcarsg  31673  eulerpartlemmf  31743  isrrvv  31811  reprinrn  31999  tgoldbachgt  32044  bnj976  32159  bnj944  32320  bnj1173  32384  bnj1321  32409  bnj1373  32412  bnj1417  32423  lfuhgr  32477  revwlk  32484  usgrgt2cycl  32490  subfacp1lem3  32542  subfacp1lem6  32545  subfacp1  32546  txpconn  32592  sconnpi1  32599  resconn  32606  cvmscbv  32618  cvmsval  32626  cvmlift2lem13  32675  cvmlift3lem2  32680  cvmlift3  32688  goeleq12bg  32709  satfvsucsuc  32725  satfbrsuc  32726  fmlafvel  32745  satffunlem2lem1  32764  satefvfmla1  32785  mclsrcl  32921  br8  33105  br6  33106  br4  33107  elintfv  33120  fv1stcnv  33133  fv2ndcnv  33134  distel  33161  frpomin  33191  poseq  33208  wsuclem  33225  sltsolem1  33293  nosupdm  33317  nosupbnd1lem4  33324  slenlt  33344  sleloe  33346  etasslt  33387  madeval2  33403  imageval  33504  funpartfv  33519  dfrdg4  33525  altopthg  33541  altopthbg  33542  brcolinear2  33632  lineext  33650  brsegle  33682  seglelin  33690  broutsideof2  33696  isfne4  33801  isfne2  33803  isfne3  33804  fneval  33813  topfneec  33816  neibastop2lem  33821  neibastop2  33822  neifg  33832  filnetlem4  33842  onsuct0  33902  bj-19.41t  34218  bj-tagcg  34421  bj-projval  34432  bj-restuni  34512  opelopabd  34556  opelopabb  34557  brabd0  34562  bj-opelid  34571  bj-ideqg  34572  bj-opelidres  34576  bj-ideqg1  34579  bj-elid6  34585  bj-isvec  34702  bj-isclm  34705  bj-isrvecd  34712  csbwrecsg  34744  csboprabg  34747  csbmpo123  34748  topdifinffinlem  34764  isbasisrelowllem1  34772  isbasisrelowllem2  34773  rdgeqoa  34787  csbfinxpg  34805  nlpineqsn  34825  wl-3xortru  34888  wl-3xorfal  34889  wl-sbrimt  34951  wl-sblimt  34952  wl-sbnf1  34956  wl-mo2df  34971  wl-eudf  34973  wl-mo2t  34976  wl-mo3t  34977  wl-ax11-lem6  34987  wl-dfclab  34993  uncov  35038  tan2h  35049  matunitlindf  35055  ptrest  35056  poimirlem2  35059  poimirlem16  35073  poimirlem19  35076  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  mbfposadd  35104  cnambfre  35105  itg2addnclem2  35109  fdc  35183  heibor1  35248  rrncmslem  35270  rrnheibor  35275  opidonOLD  35290  issmgrpOLD  35301  ismndo  35310  isrngo  35335  isdivrngo  35388  isfldidl2  35507  isdmn3  35512  releleccnv  35678  releccnveq  35679  brcnvep  35686  elecres  35694  eleccnvep  35698  ideq2  35725  extid  35728  relcnveq3  35738  eqres  35757  brrabga  35758  ecin0  35766  alrmomodm  35773  brxrn  35786  brxrn2  35787  elecxrn  35798  br1cnvxrn2  35804  elec1cnvxrn2  35805  br1cossinres  35847  br1cossxrnres  35848  eldmcoss  35858  elrels2  35886  elrelscnveq3  35891  br1cnvssrres  35905  brcnvssr  35906  dfrefrels2  35913  dfcnvrefrels2  35926  dfsymrels2  35941  elrefsymrelsrel  35967  dftrrels2  35971  erim2  36071  eldisjs5  36119  prtlem13  36164  prter3  36178  lrelat  36310  islshpat  36313  lshpsmreu  36405  lkrpssN  36459  cmtvalN  36507  omllaw2N  36540  cvrval  36565  cvrval2  36570  cvlsupr3  36640  3dim0  36753  islln2  36807  islpln5  36831  islpln2  36832  islpln2ah  36845  islvol5  36875  islvol2  36876  4atlem11  36905  pmapglbx  37065  cdleme18d  37591  cdlemefrs29bpre0  37692  cdlemb3  37902  cdlemg33b  38003  cdlemkid3N  38229  cdlemkid4  38230  dvhb1dimN  38282  dia11N  38344  cdlemm10N  38414  dib11N  38456  dib1dim  38461  dibglbN  38462  diblsmopel  38467  dihopelvalcpre  38544  dih11  38561  dihmeetlem4preN  38602  dihmeetlem13N  38615  lcfrvalsnN  38837  lcfrlem9  38846  lcf1o  38847  mapdval4N  38928  baerlem3lem2  39006  baerlem5alem2  39007  baerlem5blem2  39008  hdmap1fval  39092  hdmapfval  39123  hdmapglem7a  39223  hlhillcs  39254  19.9dev  39396  frlmfielbas  39434  fsuppind  39456  fsuppssindlem2  39458  addsubeq4com  39474  prjspreln0  39603  ellz1  39708  lzunuz  39709  fz1eqin  39710  diophrex  39716  rexrabdioph  39735  rexfrabdioph  39736  2rexfrabdioph  39737  3rexfrabdioph  39738  4rexfrabdioph  39739  6rexfrabdioph  39740  7rexfrabdioph  39741  fzneg  39923  expdioph  39964  wepwsolem  39986  fnwe2lem2  39995  islmodfg  40013  kercvrlsm  40027  cnvcnvintabd  40300  sqrtcvallem1  40331  iunrelexpuztr  40420  brtrclfv2  40428  frege124d  40462  or3or  40724  uneqsn  40726  clsk1independent  40749  ntrclsneine0lem  40767  ntrclsiso  40770  ntrclsk2  40771  ntrclskb  40772  ntrclsk3  40773  ntrclsk13  40774  ntrclsk4  40775  ntrneiel2  40789  ntrneiiso  40794  ntrneikb  40797  ntrneik3  40799  ntrneix3  40800  ntrneik13  40801  ntrneix13  40802  ntrneik4w  40803  k0004lem3  40852  scottabf  40948  pm10.52  41069  iotasbc  41123  pm14.122a  41126  pm14.122b  41127  pm14.123a  41129  rusbcALT  41143  fvsb  41156  trsbc  41246  wessf1ornlem  41811  imassmpt  41902  limcperiod  42270  limsupre  42283  dvbdfbdioo  42572  stoweidlem34  42676  fourierdlem108  42856  fourierdlem110  42858  etransc  42925  funressnfv  43635  dfafn5a  43716  ndfatafv2nrn  43777  afv2ndefb  43780  dfatsnafv2  43808  dfatdmfcoafv2  43810  dfatco  43812  afv2fv0xorb  43823  readdcnnred  43860  resubcnnred  43861  recnmulnred  43862  cndivrenred  43863  elfz2z  43872  el1fzopredsuc  43882  elsetpreimafvb  43901  iccelpart  43950  ichan  43972  ichal  43983  reupr  44039  lighneallem2  44124  dfeven2  44167  gbowge7  44281  sbgoldbwt  44295  isupwlk  44364  uspgrsprfo  44376  ismhm0  44425  inclfusubc  44491  isrnghm  44516  rnghmval2  44519  uzlidlring  44553  lidldomnnring  44554  zrninitoringc  44695  opeliun2xp  44734  snlindsntor  44880  elbigo2  44966  resum2sqorgt0  45123  rrx2pnedifcoorneor  45130  rrx2plord  45134  rrx2plordisom  45137  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  rrx2linest2  45158  itsclc0b  45186  itsclinecirc0in  45189  inlinecirc02plem  45200  gte-lte  45250  gt-lt  45251