Theorem bitrid 283

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

Hypotheses

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

Assertion

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

Proof of Theorem bitrid

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bitr2id  284  bitr3id  285  3bitr4g  314  imim21b  394  ifpfal  1075  norass  1538  ax12wdemo  2137  eu6lem  2567  abbib  2799  clelab  2874  necon3abid  2962  necon3bid  2970  ceqsralv  3475  ralxpxfr2d  3599  ceqsrexv  3608  ceqsrex2v  3611  elabgt  3625  elab2gw  3632  elab2g  3634  elrabf  3642  elrab3t  3644  eueq2  3667  eqreu  3686  reu8  3690  ruOLD  3738  sbc6g  3769  sbcieg  3779  sbcied  3783  sbcralt  3821  sbcabel  3827  rcompleq  4253  sbcel1g  4364  sbcel2  4366  csbnestgfw  4370  csbnestgf  4375  sbccsb2  4385  2nreu  4392  disjpss  4409  sbcssg  4468  2reu4lem  4470  rabsneq  4593  rexsngf  4623  reusngf  4625  ralsng  4626  rexsng  4627  elunsn  4634  el7g  4641  ralprgf  4645  rexprgf  4646  ralprg  4647  reuprg0  4653  difsn  4748  preq2b  4797  opthpr  4801  preqsnd  4809  csbopg  4841  ralunsn  4844  uniprg  4873  csbuni  4886  intprg  4929  dfiin2g  4979  iunxsng  5036  iunxsngf  5038  elpwuni  5051  disjxun  5087  sbcbr12g  5145  opthneg  5419  otthg  5423  copsex2g  5431  opeqsng  5441  snopeqop  5444  brsnop  5460  opelopabt  5470  opelopabga  5471  brabga  5472  opelopabgf  5478  csbmpt12  5495  rbropapd  5500  dfid3  5512  frirr  5590  wereu2  5611  opeliunxp  5681  opeliun2xp  5682  posn  5700  sosn  5701  frsn  5702  brab2a  5707  opbrop  5712  csbcnvgALT  5822  dmopabelb  5854  elrnmpt1  5897  elrnmptg  5898  opelres  5931  elimampt  5989  eliniseg2  6052  poleloe  6075  xpdifid  6112  cnvpo  6230  reu3op  6235  elpredgg  6257  frpomin  6283  ordtri4  6339  oneqmini  6355  elsucg  6372  elsuc2g  6373  sbcfung  6501  dffun8  6505  fncnv  6550  fununi  6552  fnssresb  6599  fnimaeq0  6610  csbfv12  6862  dffn5  6875  funimass4  6881  feqmptdf  6887  dmfco  6913  fndmdif  6970  fvimacnvi  6980  fvimacnvALT  6985  unpreima  6991  respreima  6994  fmptco  7057  fressnfv  7088  fmptsnd  7098  fnnfpeq0  7107  tpres  7130  elunirn  7180  dff13  7183  f1ounsn  7201  f12dfv  7202  f13dfv  7203  fliftel  7238  isoini  7267  f1oiso  7280  fnssintima  7291  imaeqsexvOLD  7292  riotaeqimp  7324  fnbrovb  7392  eloprabga  7450  resoprab2  7460  elimampo  7478  elrnmpores  7479  ralrnmpo  7480  ovid  7482  ov  7485  ovg  7506  imaeqexov  7579  imaeqalov  7580  ofrfval2  7626  dfwe2  7702  ssonprc  7715  ordpwsuc  7740  dfom2  7793  f1oweALT  7899  el2xptp0  7963  releldmdifi  7972  fmpox  7994  ovmptss  8018  1stconst  8025  2ndconst  8026  frxp2  8069  xpord2pred  8070  xpord3pred  8077  poseq  8083  fnsuppres  8116  suppcoss  8132  brtpos2  8157  mpocurryd  8194  csbfrecsg  8209  dfsmo2  8262  rdglim2  8346  seqomlem2  8365  omeu  8495  oeeui  8512  naddasslem1  8604  naddasslem2  8605  brdifun  8647  eqerlem  8652  elecres  8665  brecop  8729  erovlem  8732  eceqoveq  8741  mapfset  8769  mapsnd  8805  ixpsnval  8819  mptelixpg  8854  xpsnen  8969  xpdom2  8980  omxpenlem  8986  xpf1o  9047  mapunen  9054  onfin  9119  1sdom  9134  fimaxg  9166  fodomfib  9208  fodomfibOLD  9210  fofinf1o  9211  fipreima  9237  supub  9338  infglb  9370  infglbb  9371  fiming  9379  fiinfg  9380  ordtypecbv  9398  ordtypelem3  9401  ordtypelem9  9407  hartogslem1  9423  wofib  9426  wemapsolem  9431  wemapso2lem  9433  noinfep  9545  cantnf  9578  ttrclselem2  9611  ttrclse  9612  rankbnd2  9754  domtri2  9874  infxpenc2  9905  fseqdom  9909  acni2  9929  dfac9  10020  cfeq0  10139  cfsuc  10140  cflim3  10145  cfslb  10149  cofsmo  10152  enfin2i  10204  isfin3ds  10212  isf33lem  10249  fin1a2lem5  10287  axdc2lem  10331  zorn2g  10386  fodomb  10409  brdom7disj  10414  brdom6disj  10415  iundom2g  10423  cfpwsdom  10467  elgch  10505  fpwwe2cbv  10513  fpwwecbv  10527  pwfseqlem3  10543  pwfseqlem4a  10544  pwfseqlem4  10545  ltpiord  10770  nlt1pi  10789  nqereu  10812  addclprlem1  10899  1idpr  10912  reclem3pr  10932  ltsosr  10977  map2psrpr  10993  supsrlem  10994  axrrecex  11046  xrlenlt  11169  eqlei2  11216  addsubeq4  11367  renegcli  11414  lesub0  11626  wloglei  11641  conjmul  11830  rereccl  11831  infm3  12073  supaddc  12081  supadd  12082  supmul1  12083  supmullem1  12084  supmullem2  12085  supmul  12086  creui  12112  nndiv  12163  elznn0  12475  prime  12546  eqreznegel  12824  zsupss  12827  rebtwnz  12837  negelrp  12917  ltxr  13006  elixx3g  13250  ixxun  13253  ioo0  13262  ico0  13283  ioc0  13284  icc0  13285  difreicc  13376  divelunit  13386  iccf1o  13388  elfz2  13406  fzn  13432  fznn  13484  fzdif1  13497  fzshftral  13507  nelfzo  13556  fzosplitsni  13671  om2uzisoi  13853  rabssnn0fi  13885  mptnn0fsupp  13896  sq11i  14090  hashsdom  14280  fi1uzind  14406  wrdval  14415  csbwrdg  14443  wrd2ind  14622  s2f1o  14815  cjreb  15022  rexfiuz  15247  cau3lem  15254  rlim2  15395  ello12  15415  ello1mpt  15420  elo12  15426  o1lo1  15436  lo1resb  15463  o1resb  15465  o1compt  15486  caucvgb  15579  mertens  15785  ruclem12  16142  divides  16157  dvdsabseq  16216  odd2np1  16244  oddm1even  16246  sumodd  16291  divalgmod  16309  modremain  16311  sadadd2lem2  16353  gcdcllem2  16403  bezoutlem2  16443  bezoutlem3  16444  bezoutlem4  16445  isprm2  16585  isprm3  16586  dvdsnprmd  16593  oddprmdvds  16807  prmreclem2  16821  prmreclem5  16824  prmreclem6  16825  4sqlem2  16853  4sqlem12  16860  vdwmc  16882  vdwpc  16884  vdwlem6  16890  vdwlem10  16894  vdwnn  16902  ramval  16912  0ram  16924  prdsleval  17373  pwsle  17388  imasleval  17437  xpsfrnel2  17460  xpsle  17475  isacs2  17551  mreacs  17556  acsfn  17557  iscatd2  17579  catpropd  17607  ciclcl  17701  cicrcl  17702  isssc  17719  inclfusubc  17842  evlfcl  18120  uncfcurf  18137  oduleg  18188  pltval  18228  lublecllem  18256  posglbmo  18308  tosso  18315  oduclatb  18405  odudlatb  18423  isipodrs  18435  chnub  18520  gsumvalx  18576  ismhm0  18690  elefmndbas  18773  sgrp2rid2  18826  grplmulf1o  18918  grpraddf1o  18919  grplactcnv  18948  elnmz  19068  eqgid  19085  isghm  19120  isghmOLD  19121  ghmeqker  19148  resscntz  19238  cntzsgrpcl  19239  symg1bas  19296  pgrpsubgsymgbi  19313  symgfixelq  19338  f1omvdconj  19351  odmulgeq  19462  sylow3lem3  19534  sylow3lem6  19537  efgval2  19629  efgsdm  19635  efgrelexlema  19654  efgcpbllemb  19660  iscyggen2  19786  cyggenod  19789  gsummptfzcl  19874  eldprd  19911  dprdf11  19930  dprddisj2  19946  pgpfac1lem2  19982  pgpfac1  19987  srg1zr  20126  isrnghm  20352  rnghmval2  20355  issubrng  20455  issubrg  20479  zrninitoringc  20584  drngid2  20660  sdrgacs  20709  islmod  20790  rngqiprngimf1lem  21224  rngqiprngimfo  21231  pzriprnglem10  21420  zndvds  21479  znleval  21484  iunocv  21611  pjfval2  21639  pjdm2  21641  dsmmelbas  21669  ellspd  21732  islindf  21742  islindf4  21768  aspval2  21828  psrbag  21847  cply1coe0bi  22210  istopg  22803  basgen2  22897  isclo  22995  mretopd  23000  isnei  23011  isperf3  23061  restdis  23086  neitr  23088  restcls  23089  restlp  23091  restperf  23092  iscn  23143  iscnp  23145  lmbr2  23167  lmbrf  23168  ordtt1  23287  cmpsub  23308  hauscmplem  23314  cmpfi  23316  dfconn2  23327  1stcelcls  23369  1stccn  23371  nllyi  23383  subislly  23389  dissnlocfin  23437  elkgen  23444  ptpjpre1  23479  ptuni2  23484  ptclsg  23523  ptcnplem  23529  txcn  23534  hausdiag  23553  txhaus  23555  txkgen  23560  xkoptsub  23562  cnmpt21  23579  elqtop  23605  tgqtop  23620  r0cld  23646  elfg  23779  fbasrn  23792  trfil2  23795  trfil3  23796  fin1aufil  23840  elfm2  23856  elfm3  23858  flimopn  23883  fbflim  23884  flfnei  23899  flftg  23904  cnpflf2  23908  txflf  23914  fclsbas  23929  alexsubALTlem4  23958  cnextfvval  23973  snclseqg  24024  tgphaus  24025  tsmsfbas  24036  tsmssubm  24051  utopsnneip  24156  prdsxmetlem  24276  imasdsf1olem  24281  xpsdsval  24289  blres  24339  isxms2  24356  metcnp  24449  txmetcnp  24455  txmetcn  24456  metustel  24458  metuel2  24473  dscopn  24481  isngp4  24520  cnblcld  24682  metnrmlem1a  24767  icoopnst  24856  iocopnst  24857  elpi1  24965  isclmp  25017  isncvsngp  25069  lmmbr2  25179  cfil3i  25189  caucfil  25203  iscmet3  25213  lmclim  25223  metcld2  25227  bcthlem4  25247  minveclem3b  25348  minveclem6  25354  minveclem7  25355  ivthle  25377  ivthle2  25378  evthicc2  25381  ovolfioo  25388  ovolficc  25389  ovolgelb  25401  dyadmax  25519  subopnmbl  25525  ismbf3d  25575  mbfimaopnlem  25576  mbfimaopn2  25578  mbfaddlem  25581  mbfsup  25585  mbfinf  25586  i1f1lem  25610  i1fmulclem  25623  itg1climres  25635  mbfi1fseqlem4  25639  itg2monolem1  25671  itg2gt0  25681  isibl  25686  iblcnlem1  25709  ellimc2  25798  dvcnvrelem1  25942  itgsubst  25976  mdegleb  25989  fta1glem2  26094  quotval  26220  vieta1lem1  26238  vieta1lem2  26239  ulm2  26314  ulmcaulem  26323  ulmcau  26324  radcnvlt1  26347  sineq0  26453  cos11  26462  recosf1o  26464  efopn  26587  cxpeq  26687  mcubic  26777  birthdaylem3  26883  rlimcnp  26895  xrlimcnp  26898  eldmgm  26952  dmgmaddn0  26953  lgamgulmlem6  26964  wilth  27001  isppw  27044  isppw2  27045  mumullem2  27110  sqff1o  27112  mpodvdsmulf1o  27124  dvdsmulf1o  27126  fsumvma  27144  fsumvma2  27145  vmasum  27147  chpchtsum  27150  lgsne0  27266  gausslemma2dlem0i  27295  gausslemma2dlem1a  27296  lgseisenlem2  27307  lgsquadlem1  27311  lgsquadlem2  27312  2lgslem1a  27322  addsq2reu  27371  2sqreu  27387  2sqreunn  27388  2sqreult  27389  2sqreunnlt  27391  dchrmusumlema  27424  rpvmasum2  27443  dchrisum0lema  27445  pntibndlem3  27523  pntlemi  27535  pntleml  27542  pnt3  27543  sltsolem1  27607  nosupdm  27636  nosupbnd1lem4  27643  slenlt  27684  sleloe  27686  eqscut2  27740  madeval2  27787  elold  27807  addscut  27914  addsunif  27938  om2noseqiso  28225  n0scut  28255  elzs2  28316  elznns  28319  pw2cut2  28375  renegscl  28393  readdscl  28394  remulscl  28397  trgcgrg  28486  tgcgr4  28502  colcom  28529  colrot1  28530  ltgov  28568  hlcomb  28574  lncom  28593  mirreu3  28625  isperp  28683  perpcom  28684  iscgra  28780  isinag  28809  brbtwn  28870  brcgr  28871  brbtwn2  28876  colinearalg  28881  axeuclidlem  28933  axcontlem2  28936  axcontlem4  28938  axcontlem7  28941  elntg2  28956  edgiedgb  29025  isuhgr  29031  isushgr  29032  isupgr  29055  isumgr  29066  isuspgr  29123  isusgr  29124  uhgr0v0e  29209  isfusgrf1  29291  opfusgr  29294  usgr1v0e  29297  dfnbgr3  29309  nbuhgr2vtx1edgb  29323  edgnbusgreu  29338  nbusgredgeu0  29339  isuvtx  29366  cusgruvtxb  29393  cplgr3v  29406  cusgrsizeinds  29424  vtxdg0v  29445  vtxd0nedgb  29460  vtxduhgr0nedg  29464  vtxdusgr0edgnelALT  29468  iswlk  29582  wlk1walk  29610  upgr2wlk  29638  upgristrl  29672  dfpth2  29700  2pthnloop  29702  usgr2pthlem  29734  isclwlke  29748  isclwlkupgr  29749  iswwlksnx  29811  wwlksnextwrd  29868  wwlksnextproplem3  29882  2pthon3v  29914  umgr2wlk  29920  elwwlks2on  29930  elwwlks2  29937  elwspths2spth  29938  clwwlknclwwlkdif  29949  clwlkclwwlk  29972  clwlkclwwlk2  29973  clwwlkn1  30011  clwwlkn2  30014  clwwlkwwlksb  30024  eclclwwlkn1  30045  eleclclwwlkn  30046  hashecclwwlkn1  30047  umgrhashecclwwlk  30048  clwwlknonel  30065  clwwlknon1  30067  clwwlknun  30082  1pthon2v  30123  uhgr3cyclex  30152  isconngr  30159  isconngr1  30160  eupthres  30185  eupth2lems  30208  frgr0v  30232  frgr3vlem2  30244  fusgr2wsp2nb  30304  extwwlkfab  30322  numclwwlk1lem2foa  30324  numclwwlk1lem2fo  30328  isvclem  30547  isnvlem  30580  isphg  30787  isph  30792  phoeqi  30827  ubthlem3  30842  minvecolem5  30851  minvecolem6  30852  minvecolem7  30853  hhph  31148  issh3  31189  nmopub  31878  nmfnleub  31895  adjeq  31905  adjvalval  31907  elunop2  31983  lnophm  31989  nmcexi  31996  cnlnadjlem5  32041  cnlnadjeui  32047  adjbd1o  32055  jpi  32240  mddmd2  32279  chrelati  32334  chrelat2i  32335  cvexchlem  32338  dmdbr5ati  32392  cdjreui  32402  cdj3i  32411  tpssg  32507  disjunsn  32564  opeldifid  32569  fcoinvbr  32575  brab2d  32578  brabgaf  32579  opabdm  32584  opabrn  32585  iunsnima  32591  nfpconfp  32604  abfmpunirn  32624  fmptcof2  32629  funcnvmpt  32639  funcnv5mpt  32640  suppiniseg  32657  ressupprn  32661  brprop  32668  f1od2  32692  resf1o  32703  fpwrelmap  32706  iocinioc2  32752  eliccioo  32901  wrdt2ind  32924  posrasymb  32938  mgccnv  32970  gsumwun  33035  isslmd  33161  islbs5  33335  nsgqusf1olem3  33370  prmidl0  33405  ssdifidlprm  33413  crngmxidl  33424  1arithidomlem1  33490  1arithufdlem2  33500  ply1degltel  33545  ply1degleel  33546  fedgmullem2  33633  fldext2chn  33731  constrextdg2lem  33751  smatrcl  33799  rspectopn  33870  pstmxmet  33900  prsdm  33917  prsrn  33918  ordtconnlem1  33927  xrmulc1cn  33933  ispisys2  34156  elcarsg  34308  eulerpartlemmf  34378  isrrvv  34446  reprinrn  34621  tgoldbachgt  34666  bnj976  34779  bnj944  34940  bnj1173  35004  bnj1321  35029  bnj1373  35032  bnj1417  35043  fineqvrep  35105  onvf1odlem2  35116  lfuhgr  35130  revwlk  35137  usgrgt2cycl  35142  subfacp1lem3  35194  subfacp1lem6  35197  subfacp1  35198  txpconn  35244  sconnpi1  35251  resconn  35258  cvmscbv  35270  cvmsval  35278  cvmlift2lem13  35327  cvmlift3lem2  35332  cvmlift3  35340  goeleq12bg  35361  satfvsucsuc  35377  satfbrsuc  35378  fmlafvel  35397  satffunlem2lem1  35416  satefvfmla1  35437  mclsrcl  35573  ellcsrspsn  35653  br8  35768  br6  35769  br4  35770  elintfv  35777  fv1stcnv  35789  fv2ndcnv  35790  distel  35816  wsuclem  35838  imageval  35943  funpartfv  35958  dfrdg4  35964  altopthg  35980  altopthbg  35981  brcolinear2  36071  lineext  36089  brsegle  36121  seglelin  36129  broutsideof2  36135  cbvprodvw2  36260  isfne4  36353  isfne2  36355  isfne3  36356  fneval  36365  topfneec  36368  neibastop2lem  36373  neibastop2  36374  neifg  36384  filnetlem4  36394  onsuct0  36454  weiunlem2  36476  bj-19.41t  36787  bj-sbievwd  36795  bj-elgab  36952  bj-tagcg  36998  bj-projval  37009  bj-restuni  37110  opelopabd  37154  opelopabb  37155  brabd0  37160  bj-opelid  37169  bj-ideqg  37170  bj-opelidres  37174  bj-ideqg1  37177  bj-elid6  37183  bj-isvec  37300  bj-isclm  37304  bj-isrvecd  37311  csboprabg  37343  csbmpo123  37344  topdifinffinlem  37360  isbasisrelowllem1  37368  isbasisrelowllem2  37369  rdgeqoa  37383  csbfinxpg  37401  nlpineqsn  37421  wl-3xortru  37484  wl-3xorfal  37485  wl-sbid2ft  37558  wl-sbrimt  37560  wl-sblimt  37561  wl-sbnf1  37568  wl-mo2df  37583  wl-eudf  37585  wl-mo2t  37588  wl-mo3t  37589  wl-issetft  37595  wl-ax11-lem6  37603  wl-dfclab  37609  uncov  37620  tan2h  37631  matunitlindf  37637  ptrest  37638  poimirlem2  37641  poimirlem16  37655  poimirlem19  37658  poimirlem23  37662  poimirlem24  37663  poimirlem25  37664  poimirlem26  37665  poimirlem27  37666  mbfposadd  37686  cnambfre  37687  itg2addnclem2  37691  fdc  37764  heibor1  37829  rrncmslem  37851  rrnheibor  37856  opidonOLD  37871  issmgrpOLD  37882  ismndo  37891  isrngo  37916  isdivrngo  37969  isfldidl2  38088  isdmn3  38093  releleccnv  38271  releccnveq  38272  brcnvep  38279  br1cnvres  38283  eleccnvep  38294  ideq2  38320  extid  38323  relcnveq3  38334  eqres  38347  brrabga  38348  cnvref4  38357  ecin0  38359  alrmomodm  38366  brcnvin  38377  brxrn  38381  brxrn2  38382  elecxrn  38397  br1cnvxrn2  38407  elec1cnvxrn2  38408  br1cossinres  38463  br1cossxrnres  38464  eldmcoss  38474  elrels2  38502  elrelscnveq3  38507  br1cnvssrres  38521  brcnvssr  38522  dfrefrels2  38529  dfcnvrefrels2  38544  dfsymrels2  38561  elrefsymrelsrel  38587  dftrrels2  38591  erimeq2  38695  eldisjs5  38743  prtlem13  38886  prter3  38900  lrelat  39032  islshpat  39035  lshpsmreu  39127  lkrpssN  39181  cmtvalN  39229  omllaw2N  39262  cvrval  39287  cvrval2  39292  cvlsupr3  39362  3dim0  39475  islln2  39529  islpln5  39553  islpln2  39554  islpln2ah  39567  islvol5  39597  islvol2  39598  4atlem11  39627  pmapglbx  39787  cdleme18d  40313  cdlemefrs29bpre0  40414  cdlemb3  40624  cdlemg33b  40725  cdlemkid3N  40951  cdlemkid4  40952  dvhb1dimN  41004  dia11N  41066  cdlemm10N  41136  dib11N  41178  dib1dim  41183  dibglbN  41184  diblsmopel  41189  dihopelvalcpre  41266  dih11  41283  dihmeetlem4preN  41324  dihmeetlem13N  41337  lcfrvalsnN  41559  lcfrlem9  41568  lcf1o  41569  mapdval4N  41650  baerlem3lem2  41728  baerlem5alem2  41729  baerlem5blem2  41730  hdmap1fval  41814  hdmapfval  41845  hdmapglem7a  41945  hlhillcs  41976  19.9dev  42226  addsubeq4com  42292  ef11d  42351  frlmfielbas  42512  fsuppind  42602  fsuppssindlem2  42604  prjspreln0  42621  ellz1  42779  lzunuz  42780  fz1eqin  42781  diophrex  42787  rexrabdioph  42806  rexfrabdioph  42807  2rexfrabdioph  42808  3rexfrabdioph  42809  4rexfrabdioph  42810  6rexfrabdioph  42811  7rexfrabdioph  42812  fzneg  42994  expdioph  43035  wepwsolem  43054  fnwe2lem2  43063  islmodfg  43081  kercvrlsm  43095  unielss  43230  ordeldif  43270  ordeldifsucon  43271  ordeldif1o  43272  nnoeomeqom  43324  cantnfresb  43336  tfsconcatrev  43360  nadd1suc  43404  naddgeoa  43406  minregex  43546  cnvcnvintabd  43612  sqrtcvallem1  43643  iunrelexpuztr  43731  brtrclfv2  43739  frege124d  43773  or3or  44035  uneqsn  44037  clsk1independent  44058  ntrclsneine0lem  44076  ntrclsiso  44079  ntrclsk2  44080  ntrclskb  44081  ntrclsk3  44082  ntrclsk13  44083  ntrclsk4  44084  ntrneiel2  44098  ntrneiiso  44103  ntrneikb  44106  ntrneik3  44108  ntrneix3  44109  ntrneik13  44110  ntrneix13  44111  ntrneik4w  44112  k0004lem3  44161  scottabf  44252  pm10.52  44377  iotasbc  44431  pm14.122a  44434  pm14.122b  44435  pm14.123a  44437  rusbcALT  44450  fvsb  44463  trsbc  44552  ssabso  44986  disjabso  44987  pwclaxpow  44996  modelac8prim  45004  permaxrep  45018  wessf1ornlem  45201  imassmpt  45278  caucvgbf  45506  rexanuz2nf  45509  limcperiod  45647  limsupre  45658  dvbdfbdioo  45947  stoweidlem34  46051  fourierdlem108  46231  fourierdlem110  46233  etransc  46300  funressnfv  47053  dfafn5a  47170  ndfatafv2nrn  47231  afv2ndefb  47234  dfatsnafv2  47262  dfatdmfcoafv2  47264  dfatco  47266  afv2fv0xorb  47277  readdcnnred  47313  resubcnnred  47314  recnmulnred  47315  cndivrenred  47316  elfz2z  47325  el1fzopredsuc  47335  elsetpreimafvb  47394  iccelpart  47443  ichan  47465  ichal  47476  reupr  47532  lighneallem2  47616  dfeven2  47659  gbowge7  47773  sbgoldbwt  47787  dfclnbgr3  47836  clnbgrel  47838  clnbupgrel  47844  isubgredg  47876  uhgrimedgi  47900  isuspgrim0  47904  dfgric2  47925  clnbgrgrimlem  47943  grimedg  47945  grtriprop  47951  usgrgrtrirex  47960  stgrnbgr0  47974  isubgr3stgrlem7  47982  uspgrlimlem1  47998  dfgrlic2  48018  dfgrlic3  48020  gpgvtxel  48057  gpgedgel  48060  pgnbgreunbgrlem4  48129  isupwlk  48146  uspgrsprfo  48158  uzlidlring  48245  lidldomnnring  48246  snlindsntor  48482  elbigo2  48563  resum2sqorgt0  48720  rrx2pnedifcoorneor  48727  rrx2plord  48731  rrx2plordisom  48734  eenglngeehlnmlem1  48748  eenglngeehlnmlem2  48749  rrx2linest2  48755  itsclc0b  48783  itsclinecirc0in  48786  inlinecirc02plem  48797  brab2dd  48838  fvconstr  48872  fvconstrn0  48873  opndisj  48913  clddisj  48914  i0oii  48930  io1ii  48931  fucofulem2  49322  isthincd2lem1  49436  functhinc  49459  isinito2lem  49509  isinito4  49558  lmdran  49682  cmdlan  49683  gte-lte  49735  gt-lt  49736