Theorem 3eqtr3d 2780

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr3d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3d	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3d

Step	Hyp	Ref	Expression
1		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3	1, 2	eqtr3d 2774	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	eqtr3d 2774	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  reldisjun  6032  mpteqb  7017  fvmptt  7018  fvsnun2  7180  fsnunfv  7184  f1ocnvfv1  7273  f1ocnvfv2  7274  fcof1  7284  f1ofvswap  7303  weniso  7350  caov12d  7627  caov13d  7629  caov411d  7631  caovmo  7643  onovuni  8341  tfrlem5  8379  seqomlem1  8449  seqomlem4  8452  onasuc  8527  onesuc  8529  oeeui  8601  nadd4  8696  fopwdom  9079  unxpdomlem2  9250  cantnfres  9671  cnfcom2lem  9695  cnfcom2  9696  updjud  9928  cardiun  9976  ackbij1lem16  10229  ackbij2lem2  10234  fpwwe2lem5  10629  fpwwe2lem7  10631  canthp1lem2  10647  mul12  11378  mul4  11381  addrid  11393  addcan  11397  addcom  11399  addcomd  11415  add12  11430  ppncan  11501  addsub4  11502  subeqxfrd  11622  subaddeqd  11628  muladd  11645  mulcand  11846  receu  11858  div13  11892  divdivdiv  11914  divcan5  11915  divdiv1  11924  divdiv2  11925  halfaddsub  12444  xadddi  13273  xov1plusxeqvd  13474  fztp  13556  flzadd  13790  fldiv  13824  mulp1mod1  13876  modnegd  13890  modsub12d  13892  2submod  13896  seqm1  13984  seqcaopr  14004  seqf1o  14008  exprec  14068  expsub  14075  zesq  14188  digit1  14199  discr1  14201  discr  14202  facnn2  14241  faclbnd6  14258  hashfz1  14305  hashdom  14338  hashun  14341  hashbclem  14410  hashfac  14418  seqcoll  14424  ccatopth  14665  repsw2  14900  repsw3  14901  shftval3  15022  crre  15060  resub  15073  imsub  15081  cjsub  15095  nn0sqeq1  15222  abslem2  15285  sqreulem  15305  bhmafibid1  15411  climshft2  15525  isercolllem2  15611  iseraltlem2  15628  iseraltlem3  15629  fsumsub  15733  telfsumo  15747  telfsumo2  15748  hashiun  15767  bcxmas  15780  climcndslem1  15794  climcndslem2  15795  trireciplem  15807  geoser  15812  geo2sum2  15819  fprodm1  15910  fallfacfwd  15979  binomfallfaclem2  15983  bpolydiflem  15997  bpoly4  16002  fsumcube  16003  sinsub  16110  cossub  16111  rpnnen2lem10  16165  ruclem12  16183  p1modz1  16203  mod2eq1n2dvds  16289  pwp1fsum  16333  divalglem9  16343  bitsinv1lem  16381  bitsinv1  16382  bitsf1  16386  sadasslem  16410  bitsres  16413  smup1  16429  smumul  16433  modgcd  16473  absmulgcd  16490  eucalg  16523  lcmgcd  16543  lcmid  16545  lcmftp  16572  numdensq  16689  dfphi2  16706  phiprm  16709  fermltl  16716  prmdiveq  16718  hashgcdlem  16720  odzdvds  16727  powm2modprm  16735  modprm0  16737  coprimeprodsq  16740  pythagtriplem6  16753  pythagtriplem7  16754  pythagtriplem12  16758  pythagtriplem16  16762  pcaddlem  16820  sumhash  16828  pcfac  16831  pockthlem  16837  prmreclem6  16853  4sqlem12  16888  4sqlem15  16891  vdwlem3  16915  vdwlem6  16918  vdwlem9  16921  ramub1lem2  16959  cshwshashlem2  17029  qusaddvallem  17496  xpsaddlem  17518  xpsvsca  17522  mrcun  17565  homfeqval  17640  comfeqval  17651  sectcan  17701  sectco  17702  sectmon  17728  monsect  17729  funcsect  17821  setcmon  18036  resscatc  18058  catciso  18060  evlfcllem  18173  curf2cl  18183  curfcl  18184  yonedalem4c  18229  yonedalem3b  18231  yonedainv  18233  latj12  18436  grprinvlem  18591  grpinva  18592  grprida  18593  mnd12g  18637  resmhm  18700  pwsco2mhm  18713  frmdup3lem  18746  grprcan  18857  grplcan  18884  grpasscan1  18885  grpinv11  18891  grpinvnz  18893  grplmulf1o  18896  grpinvpropd  18897  grpinvadd  18900  grpsubsub4  18915  dfgrp3  18921  imasgrp2  18937  mhmid  18945  mhmmnd  18946  mulgz  18981  mulgdirlem  18984  mulgdir  18985  mulgass  18990  mulgsubdir  18993  mulgpropd  18995  pwsmulg  18998  isnsg3  19039  nmzsubg  19044  ssnmz  19045  eqger  19057  eqglact  19058  qus0subgadd  19075  cyccom  19079  ghminv  19098  conjnmz  19125  subgga  19163  gasubg  19165  galcan  19167  gacan  19168  cntzsubg  19202  cntzmhm  19204  symgvalstruct  19263  symgvalstructOLD  19264  psgnunilem2  19362  psgnuni  19366  sylow1lem1  19465  sylow2blem2  19488  sylow2blem3  19489  lsmmod  19542  lsmpropd  19544  lsmdisj2  19549  subgdisj1  19558  subgdisj2  19559  efgredleme  19610  efgredlemd  19611  efgredlemc  19612  efgredlem  19614  frgpup3lem  19644  mulgdi  19693  ghmcmn  19698  lsm4  19727  gsummhm2  19806  gsumpt  19829  gsum2d  19839  gsumcom3  19845  dprdfeq0  19891  ablfac1eu  19942  ablsimpgprmd  19984  rglcom4d  20033  ringcom  20096  isringd  20104  ringlz  20106  ringrz  20107  ring1eq0  20109  ringmneg1  20115  gsumdixp  20130  pwsexpg  20141  unitgrp  20196  irredrmul  20240  rhmunitinv  20289  subrginv  20334  subrgunit  20336  drngmul0or  20385  isdrngd  20389  primefld  20420  abvrec  20443  srngnvl  20463  srngadd  20464  srngmul  20465  issrngd  20468  lmodvs0  20505  lmodvneg1  20514  lmodcom  20517  lmodsubdi  20528  lmodvsinv  20646  lmodvsinv2  20647  lmhmvsca  20655  lvecvs0or  20720  lvecinv  20725  lspsnvs  20726  lspabs2  20732  lspfixed  20740  lspsolv  20755  unitrrg  20908  prmirredlem  21041  mulgrhm2  21047  chrrhm  21082  znidomb  21116  psgnghm  21132  psgninv  21134  zrhpsgnodpm  21144  evpmodpmf1o  21148  psgndiflemB  21152  ip0r  21189  ipdir  21191  ipdi  21192  ipass  21197  ipassr  21198  phlpropd  21207  ocvpj  21271  uvcresum  21347  lmimlbs  21390  asclpropd  21450  psrass1lemOLD  21492  psrass1lem  21495  psrlidm  21522  psrridm  21523  mvrf1  21544  mplmon2mul  21629  evlslem1  21644  evlseu  21645  evlssca  21651  evlsvar  21652  coe1pwmul  21800  pf1ind  21873  mat0dimbas0  21967  mdetrlin  22103  mdetrsca  22104  mdetr0  22106  mdetunilem8  22120  mdetuni0  22122  mdetmul  22124  maducoeval2  22141  madurid  22145  madulid  22146  matinv  22178  matunit  22179  slesolinv  22181  slesolinvbi  22182  cpmadugsumlemF  22377  restin  22669  cncmp  22895  cmpsublem  22902  conndisj  22919  cnconn  22925  kgencmp2  23049  ufldom  23465  tgplacthmeo  23606  ghmcnp  23618  qustgpopn  23623  qustgphaus  23626  tsmsxplem2  23657  tususp  23776  xpsdsval  23886  blpnfctr  23941  xmssym  23970  ressxms  24033  isngp2  24105  ngppropd  24145  nminvr  24185  blcvx  24313  icccvx  24465  pcohtpylem  24534  pcohtpy  24535  clmvscom  24605  cvsmuleqdivd  24649  cvsdiveqd  24650  pjthlem1  24953  ovollb2lem  25004  ovolicc2lem1  25033  ovolicc2lem5  25037  volsup  25072  ovolioo  25084  uniiccdif  25094  uniioombllem3  25101  uniioombllem4  25102  vitalilem3  25126  itg1sub  25226  itg2const  25257  iblcnlem1  25304  itgcnlem  25306  itgaddlem2  25340  itgsub  25342  itgabs  25351  ditgsplit  25377  dvmulbr  25455  dvcmul  25460  dvcmulf  25461  dvrec  25471  dvmptres3  25472  dvmptadd  25476  dvmptmul  25477  dvmptres2  25478  dvmptneg  25482  dvmptsub  25483  dvmptcj  25484  dvmptco  25488  dveflem  25495  dvlip  25509  dvlipcn  25510  dvlip2  25511  dvcvx  25536  dvfsumle  25537  dvfsumabs  25539  dvfsumlem1  25542  dvfsumlem2  25543  ftc2  25560  ftc2ditglem  25561  itgparts  25563  itgsubstlem  25564  itgsubst  25565  itgpowd  25566  fta1glem1  25682  fta1blem  25685  plyeq0lem  25723  plymullem1  25727  coeeulem  25737  coe0  25769  coesub  25770  dvply1  25796  plydivlem4  25808  plyrem  25817  fta1lem  25819  vieta1  25824  plyexmo  25825  elqaalem2  25832  aareccl  25838  aannenlem1  25840  aaliou3lem2  25855  dvtaylp  25881  taylthlem1  25884  radcnvlem1  25924  pserdvlem2  25939  efcvx  25960  ptolemy  26005  tangtx  26014  efif1olem3  26052  efif1olem4  26053  efabl  26058  lognegb  26097  efiarg  26114  cosargd  26115  tanarg  26126  logtayl  26167  cxpneg  26188  cxpsub  26189  cxprec  26193  cxproot  26197  cxpsqrt  26210  cxpcom  26244  cxpcn3lem  26252  cxpaddlelem  26256  abscxpbnd  26258  root1eq1  26260  cxpeq  26262  logrec  26265  isosctrlem2  26321  isosctrlem3  26322  isosctr  26323  ssscongptld  26324  chordthmlem  26334  heron  26340  quad2  26341  dcubic1lem  26345  mcubic  26349  cubic2  26350  cubic  26351  dquartlem2  26354  dquart  26355  quart1lem  26357  quart1  26358  asinlem2  26371  asinlem3  26373  asinsin  26394  sinacos  26407  atanlogsublem  26417  efiatan2  26419  2efiatan  26420  tanatan  26421  atantan  26425  atans2  26433  dvatan  26437  atantayl  26439  atantayl2  26440  log2cnv  26446  rlimcnp2  26468  cxplim  26473  cxp2lim  26478  cvxcl  26486  scvxcvx  26487  zetacvg  26516  lgamgulmlem4  26533  lgamcvg2  26556  gamp1  26559  wilthlem1  26569  wilthlem2  26570  ftalem5  26578  basellem3  26584  basellem5  26586  basellem8  26589  mumullem2  26681  musum  26692  musumsum  26693  muinv  26694  sgmppw  26697  1sgmprm  26699  1sgm2ppw  26700  ppiub  26704  logfac2  26717  chpchtsum  26719  perfectlem1  26729  perfectlem2  26730  dchrn0  26750  dchrfi  26755  dchrabs  26760  dchrptlem1  26764  dchrhash  26771  dchr2sum  26773  sum2dchr  26774  bposlem6  26789  bposlem9  26792  lgsvalmod  26816  lgsdilem  26824  lgsne0  26835  lgssq  26837  lgssq2  26838  lgsqr  26851  lgsdchrval  26854  lgsdchr  26855  gausslemma2dlem6  26872  gausslemma2d  26874  lgseisenlem1  26875  lgseisenlem2  26876  lgseisenlem4  26878  lgsquadlem1  26880  lgsquadlem3  26882  lgsquad3  26887  m1lgs  26888  2sqmod  26936  rplogsumlem1  26984  rplogsumlem2  26985  dchrisumlem2  26990  dchrisum0fno1  27011  rpvmasum2  27012  dchrisum0lem1  27016  dchrisum0lem2  27018  mudivsum  27030  mulog2sumlem1  27034  vmalogdivsum  27039  2vmadivsumlem  27040  logsqvma  27042  selberglem1  27045  selberglem2  27046  selberg2lem  27050  selberg3lem1  27057  selberg4lem1  27060  selberg4  27061  pntrsumo1  27065  selbergr  27068  selberg34r  27071  pntrlog2bndlem3  27079  pntrlog2bndlem4  27080  pntibndlem2  27091  pntlemg  27098  pntlemr  27102  pntlemf  27105  ostthlem1  27127  padicabvcxp  27132  ostth3  27138  nolesgn2o  27171  nolesgn2ores  27172  nogesgn1o  27173  nogesgn1ores  27174  nodenselem5  27188  nolt02o  27195  nogt01o  27196  nosupprefixmo  27200  noinfprefixmo  27201  sltlpss  27398  adds12d  27488  adds4d  27489  addsdilem3  27605  mulnegs1d  27612  muls12d  27630  norecdiv  27635  tgcgrcomlr  27728  tgifscgr  27756  iscgrglt  27762  tgbtwnconn1lem2  27821  tgbtwnconn1lem3  27822  mirne  27915  miduniq2  27935  krippenlem  27938  ragcgr  27955  cgrg3col4  28101  f1otrg  28119  ttgcontlem1  28139  brbtwn2  28160  axsegconlem10  28181  ax5seglem3  28186  ax5seglem6  28189  axpaschlem  28195  axeuclidlem  28217  axcontlem2  28220  axcontlem7  28225  axcontlem8  28226  cusgrsizeindslem  28705  frgrncvvdeq  29559  numclwwlk7  29641  grpoidinvlem1  29752  grpoideu  29757  grporcan  29766  grpolcan  29778  grpoinvop  29781  ablo4  29798  nvscom  29877  nvmul0or  29898  nvz0  29916  smcnlem  29945  ipidsq  29958  sspz  29983  lno0  30004  lnoadd  30006  lnomul  30008  ipasslem3  30081  dipdi  30091  dipassr  30094  dipsubdi  30097  ubthlem2  30119  hvmul0or  30273  hvadd12  30283  hvadd4  30284  hvmulcom  30291  normneg  30392  pjhthlem1  30639  chj12  30782  spanunsni  30827  5oalem2  30903  3oalem2  30911  hoadd4  31032  homul12  31053  hosubdi  31056  honegsubdi  31058  hosub4  31061  adj2  31182  lnopmul  31215  lnopaddi  31219  lnfnaddi  31291  lnfnmuli  31292  cnlnadjlem6  31320  adjeq0  31339  leopmul  31382  opsqrlem1  31388  opsqrlem6  31393  hstnmoc  31471  strlem1  31498  chirredlem3  31640  2ndresdju  31869  suppovss  31901  cosnop  31912  fpwrelmapffslem  31952  xaddeq0  31961  bcm1n  32001  divnumden2  32019  xmulcand  32082  xreceu  32083  s3f1  32108  ccatf1  32110  wrdt2ind  32112  swrdf1  32115  xrsmulgzz  32174  xrge0adddir  32188  xrge0adddi  32189  abliso  32192  gsumhashmul  32203  ogrpaddltrbid  32233  ogrpinvlt  32236  symgcom  32239  cyc2fv1  32275  cyc2fv2  32276  cycpmco2rn  32279  cycpmco2lem5  32284  cycpmco2lem6  32285  cycpmco2lem7  32286  cyc3fv1  32291  cyc3fv2  32292  cyc3fv3  32293  cycpmconjvlem  32295  cycpmconjslem2  32309  cycpmconjs  32310  cyc3conja  32311  archiabllem1a  32332  archiabllem1  32334  archiabllem2c  32336  slmdvs0  32365  dvrcan5  32380  ringinveu  32389  ornglmullt  32420  orngrmullt  32421  qusvsval  32462  imaslmod  32463  qustriv  32471  fermltlchr  32473  znfermltl  32474  quslsm  32511  qus0g  32513  nsgmgclem  32517  ghmquskerlem1  32523  rhmquskerlem  32538  qsidomlem2  32567  mxidlprm  32581  mxidlirredi  32582  opprqusbas  32597  qsdrngilem  32603  evls1fpws  32641  evls1addd  32643  evls1muld  32644  evls1vsca  32645  ressply10g  32651  ply1fermltlchr  32657  ply1fermltl  32658  sradrng  32668  drgext0gsca  32674  rlmdim  32689  rgmoddimOLD  32690  matdim  32695  ply1degltdimlem  32702  ply1degltdim  32703  lbsdiflsp0  32706  dimkerim  32707  fedgmullem1  32709  fedgmullem2  32710  fedgmul  32711  extdg1id  32737  ccfldextdgrr  32741  minplyirred  32765  mdetpmtr2  32799  madjusmdetlem1  32802  mdetlap  32807  qtophaus  32811  zarcmplem  32856  qqhval2lem  32956  esumpad  33048  esummulc1  33074  esumsup  33082  measxun2  33203  measssd  33208  inelcarsg  33305  carsggect  33312  carsgclctunlem2  33313  pmeasmono  33318  oddpwdc  33348  eulerpartlemgs2  33374  eulerpartlemn  33375  totprobd  33420  signstfvn  33575  signstfveq0  33583  ftc2re  33605  itgexpif  33613  breprexpnat  33641  circlemethnat  33648  circlevma  33649  circlemethhgt  33650  hgt750lemf  33660  hgt750lemg  33661  hgt750lemb  33663  tgoldbachgt  33670  bnj1379  33836  bnj1321  34033  revpfxsfxrev  34101  revwlk  34110  subfaclim  34174  cvxsconn  34229  resconn  34232  cvmliftmolem1  34267  cvmliftlem7  34277  cvmliftlem13  34282  cvmlift2lem7  34295  cvmlift3lem5  34309  elmsta  34534  msubff1  34542  mthmpps  34568  bcm1nt  34702  faclim2  34713  funsseq  34734  gg-dvmulbr  35170  gg-dvfsumle  35177  gg-dvfsumlem2  35178  clsun  35208  topjoin  35245  bj-bary1lem  36186  irrdifflemf  36201  finxpreclem4  36270  matunitlindflem1  36479  ptrest  36482  poimirlem4  36487  poimirlem6  36489  poimirlem7  36490  poimirlem9  36492  poimirlem11  36494  poimirlem12  36495  poimirlem26  36509  poimirlem27  36510  itg2addnclem  36534  itg2addnclem3  36536  itgaddnclem2  36542  itgsubnc  36545  iblmulc2nc  36548  itgabsnc  36552  ftc2nc  36565  areacirclem1  36571  areacirclem4  36574  areacirc  36576  cocanfo  36582  ablo4pnp  36743  rngolz  36785  rngorz  36786  zerdivemp1x  36810  crngm4  36866  crngohomfo  36869  lfl0  37930  lfladd  37931  lflmul  37933  eqlkr3  37966  olm11  38092  latm12  38095  cmtcomlemN  38113  omlspjN  38126  hlatj12  38236  1cvrjat  38341  dalemrotyz  38524  padd12N  38705  pmapjlln1  38721  atmod2i1  38727  pmapocjN  38796  pnonsingN  38799  pexmidN  38835  lhp2at0  38898  lhpelim  38903  ltrncnv  39012  cdleme7c  39111  cdleme15b  39141  cdlemednpq  39165  cdleme20m  39189  cdleme22cN  39208  cdleme22d  39209  cdleme23b  39216  cdleme30a  39244  cdleme35h  39322  cdlemeg46frv  39391  cdlemg2fv2  39466  cdlemg2l  39469  cdlemg2m  39470  cdlemg8c  39495  cdlemg10bALTN  39502  cdlemg12  39516  cdlemg13a  39517  cdlemg18c  39546  cdlemg19  39550  trlcoat  39589  cdlemg47  39602  tendo1ne0  39694  cdlemk9  39705  cdlemk9bN  39706  dia2dimlem1  39930  tendolinv  39971  tendorinv  39972  dvhlveclem  39974  doca3N  39993  dihmeetlem7N  40176  dihjatc1  40177  dihmeetlem18N  40190  dochnoncon  40257  dihjatc  40283  dihjatcclem1  40284  dihjatcclem4  40287  dochsnkr  40338  lcfl7lem  40365  lcfl8  40368  lcfl9a  40371  lclkrlem1  40372  lclkrlem2e  40377  lclkrlem2j  40382  lcfrlem1  40408  lcfrlem9  40416  lcfrlem23  40431  lcfrlem31  40439  mapd0  40531  mapdpglem21  40558  baerlem3lem1  40573  baerlem5alem1  40574  mapdindp4  40589  mapdh6gN  40608  hdmap1l6g  40682  hgmapval0  40758  hgmaprnlem1N  40762  hlhilhillem  40830  crng12d  41090  imacrhmcl  41091  drngmulcanad  41101  drngmulcan2ad  41102  drnginvmuld  41103  evlsbagval  41140  sn-1ne2  41181  oddnumth  41209  sumcubes  41211  exp11d  41216  numdenexp  41228  resubeulem2  41250  resubidaddlidlem  41268  sn-00idlem1  41272  readdcan2  41286  sn-negex12  41290  sn-addcand  41293  remulinvcom  41306  remullid  41307  remulcand  41312  sn-0tie0  41313  zaddcomlem  41325  zaddcom  41326  zmulcomlem  41329  zmulcom  41330  retire  41341  cnreeu  41342  prjspner1  41369  dffltz  41377  flt4lem5f  41400  flt4lem7  41402  fltnltalem  41405  fltnlta  41406  diophrw  41487  eldioph2lem1  41488  pellexlem2  41558  pellexlem6  41562  pellex  41563  pell1234qrne0  41581  pell1234qrreccl  41582  pell1qrgaplem  41601  rmxm1  41663  oddcomabszz  41673  jm2.19lem1  41718  jm3.1lem2  41747  dnnumch3  41779  pwssplit4  41821  flcidc  41906  deg1mhm  41939  dflim5  42069  omabs2  42072  sqrtcval  42382  radcnvrat  43063  nzprmdif  43068  hashnzfz  43069  dvsconst  43079  dvsid  43080  expgrowth  43084  bccm1k  43091  bccn1  43093  binomcxplemnotnn0  43105  subadd4b  43982  uzinico2  44265  sumnnodd  44336  limsupresuz  44409  limsupequzlem  44428  liminfresre  44485  liminfresuz  44490  climliminflimsupd  44507  icccncfext  44593  dvresntr  44624  itgsinexplem1  44660  itgsinexp  44661  stoweidlem1  44707  wallispi2lem2  44778  stirlinglem3  44782  stirlinglem5  44784  stirlinglem10  44789  stirlinglem15  44794  dirkertrigeqlem3  44806  dirkercncflem2  44810  fourierdlem26  44839  fourierdlem42  44855  fourierdlem66  44878  fourierdlem73  44885  fourierdlem81  44893  fourierdlem83  44895  fourierdlem107  44919  etransclem23  44963  meaiininclem  45192  vonvolmbl  45367  iccvonmbllem  45384  sigaradd  45572  cevathlem1  45573  imarnf1pr  45980  m1mod0mod1  46027  fmtnorec3  46206  proththd  46272  perfectALTVlem1  46379  perfectALTVlem2  46380  rnglz  46654  rngrz  46655  isrngd  46662  rngisom1  46708  rngqiprnglinlem1  46766  rng2idl1cntr  46780  pw2m1lepw2m1  47191  nnpw2pmod  47259  dignn0flhalflem1  47291  affinecomb2  47379  1subrec1sub  47381  eenglngeehlnmlem1  47413  2itscplem3  47456  restcls2  47536  aacllem  47838  amgmlemALT  47840  young2d  47842