Theorem syl5bi 244

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 12-Jan-1993.)

Hypotheses

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

Assertion

Ref	Expression
syl5bi	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5bi

Step	Hyp	Ref	Expression
1		syl5bi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 218	. 2 ⊢ (𝜑 → 𝜓)
3		syl5bi.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr4g  298  3orel1  1087  ax13  2393  2euexv  2716  2euex  2726  eqneqall  3027  necon3bd  3030  pm2.61dne  3103  elnelall  3136  spcimgft  3586  rspc  3611  rspcimdv  3613  rspc2gv  3632  euind  3715  reuind  3744  2reurex  3750  sbciegft  3808  rspsbc  3862  elneeldif  3950  ssexnelpss  4090  ralnralall  4458  pwpw0  4746  sssn  4759  prnebg  4786  pwsnOLD  4831  intss1  4891  intmin  4896  uniintsn  4913  iinss  4980  iinss2  4981  disji2  5048  disjiun  5053  disjiund  5056  disjxiun  5063  trel3  5180  trin  5182  eusvnfb  5294  reusv3  5306  axprlem2  5325  copsexgw  5381  copsexg  5382  propeqop  5397  otiunsndisj  5410  iunopeqop  5411  po3nr  5488  fri  5517  wefrc  5549  wereu2  5552  ssrelrel  5669  relop  5721  iss  5903  poirr2  5984  xpcan  6033  xpcan2  6034  sossfld  6043  wfi  6181  wfis2fg  6185  onfr  6230  onmindif  6280  iotan0  6345  funopg  6389  funssres  6398  funun  6400  fv3  6688  fvmptt  6788  iinpreima  6837  fvn0ssdmfun  6842  dff3  6866  dff4  6867  fmptsng  6930  fmptsnd  6931  tpres  6963  fnprb  6971  fntpb  6972  fvclss  7001  fpropnf1  7025  isomin  7090  isofrlem  7093  weniso  7107  oprabidw  7187  oprabid  7188  ssorduni  7500  onmindif2  7527  limuni3  7567  tfis2f  7570  tfinds  7574  tfinds2  7578  tfinds3  7579  funcnvuni  7636  f1oweALT  7673  funeldmdif  7747  f1o2ndf1  7818  poxp  7822  soxp  7823  fnse  7827  suppimacnv  7841  mpoxopynvov0g  7880  reldmtpos  7900  rntpos  7905  wfrlem14  7968  wfrlem15  7969  onfununi  7978  smoiun  7998  tfrlem1  8012  tfr3  8035  frsucmptn  8074  tz7.49  8081  oaordi  8172  oawordeulem  8180  omeulem1  8208  oeordi  8213  oelimcl  8226  nnaordi  8244  nneob  8279  omsmolem  8280  erdisj  8341  qsss  8358  uniinqs  8377  map0g  8448  resixpfo  8500  ixpsnf1o  8502  xpdom3  8615  mapdom3  8689  phplem4  8699  php3  8703  unxpdomlem3  8724  ssfi  8738  findcard2  8758  findcard3  8761  frfi  8763  isfiniteg  8778  xpfi  8789  fiint  8795  finsschain  8831  dffi2  8887  marypha1lem  8897  marypha2  8903  supmo  8916  suplub2  8925  infmo  8959  ordiso2  8979  ordtypelem7  8988  ordtypelem8  8989  brwdom2  9037  unxpwdom2  9052  ixpiunwdom  9055  elirrv  9060  suc11reg  9082  noinfep  9123  cantnfle  9134  cantnflem1  9152  cantnf  9156  trcl  9170  epfrs  9173  rankpwi  9252  rankunb  9279  rankuni2b  9282  rankxplim3  9310  cplem1  9318  karden  9324  carddom2  9406  fseqenlem2  9451  ac10ct  9460  acni2  9472  acndom  9477  infpwfien  9488  alephordi  9500  alephord  9501  iunfictbso  9540  aceq3lem  9546  dfac5  9554  dfac2b  9556  dfac12lem3  9571  dfac12r  9572  cdainflem  9613  cfub  9671  cfeq0  9678  coflim  9683  cfslb2n  9690  cofsmo  9691  coftr  9695  infpssr  9730  fin23lem7  9738  fin23lem11  9739  fin23lem21  9761  isf32lem2  9776  isf34lem4  9799  isfin1-2  9807  isfin1-3  9808  fin1a2lem9  9830  fin1a2lem11  9832  fin1a2lem12  9833  fin1a2lem13  9834  domtriomlem  9864  axdc3lem2  9873  axcclem  9879  ac6c4  9903  zorn2lem4  9921  zorn2lem5  9922  zorn2lem7  9924  ttukeylem5  9935  ttukeyg  9939  brdom6disj  9954  fnrndomg  9958  iunfo  9961  iundom2g  9962  ficard  9987  konigthlem  9990  alephval2  9994  pwcfsdom  10005  fpwwe2lem9  10060  fpwwe2lem11  10062  fpwwe2lem12  10063  fpwwe2lem13  10064  pwfseqlem3  10082  gchpwdom  10092  winalim2  10118  gchina  10121  wunex2  10160  tskr1om2  10190  tskxpss  10194  inar1  10197  tskuni  10205  gruun  10228  grudomon  10239  grur1  10242  ltmpi  10326  ltexprlem2  10459  ltexprlem6  10463  reclem2pr  10470  reclem3pr  10471  reclem4pr  10472  suplem1pr  10474  mulgt0sr  10527  supsrlem  10533  axrrecex  10585  axpre-sup  10591  ltlen  10741  addid0  11059  negn0  11069  negf1o  11070  mulge0b  11510  supaddc  11608  supadd  11609  supmul1  11610  supmullem1  11611  supmullem2  11612  supmul  11613  cju  11634  nnsub  11682  0mnnnnn0  11930  un0addcl  11931  un0mulcl  11932  nn0sub  11948  nn0n0n1ge2b  11964  zle0orge1  11999  peano5uzi  12072  eluzuzle  12253  zsupss  12338  elpq  12375  qbtwnre  12593  xrsupexmnf  12699  xrinfmexpnf  12700  xrsupsslem  12701  xrinfmsslem  12702  xrub  12706  supxrun  12710  ixxdisj  12754  icodisj  12863  difreicc  12871  uzsubsubfz  12930  fzadd2  12943  elfzmlbp  13019  fzofzim  13085  elfznelfzo  13143  injresinj  13159  subfzo0  13160  flval3  13186  modirr  13311  modsumfzodifsn  13313  addmodlteq  13315  ssnn0fi  13354  seqf1o  13412  expcl2lem  13442  expnegz  13464  expaddz  13474  expmulz  13476  facwordi  13650  faclbnd4lem4  13657  bccl  13683  hashnfinnn0  13723  hashgt12el  13784  hashgt12el2  13785  hashfun  13799  hashbclem  13811  hashbc  13812  hashfacen  13813  hashf1lem1  13814  hashf1  13816  hash2pwpr  13835  fundmge2nop0  13851  fi1uzind  13856  brfi1indALT  13859  swrdnd0  14019  wrdind  14084  wrd2ind  14085  swrdccatin1  14087  swrdccatin2  14091  pfxccat3  14096  pfxccat3a  14100  swrdccat3blem  14101  reuccatpfxs1  14109  cshw1  14184  cshwcsh2id  14190  wwlktovfo  14322  s3iunsndisj  14328  rtrclreclem3  14419  dfrtrcl2  14421  sqrlem1  14602  sqrlem6  14607  rexanre  14706  cau3lem  14714  2clim  14929  summo  15074  fsum2dlem  15125  fsumiun  15176  prodmo  15290  fprod2dlem  15334  bpolycl  15406  rpnnen2lem12  15578  odd2np1lem  15689  oddge22np1  15698  sqoddm1div8z  15703  sumeven  15738  pwp1fsum  15742  bitsfzo  15784  sadcaddlem  15806  gcd0id  15867  algcvgblem  15921  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem2  15984  coprmproddvdslem  16006  divgcdcoprm0  16009  isprm7  16052  prmdvdsexpr  16061  prmfac1  16063  qnumdencl  16079  hashdvds  16112  prm23lt5  16151  pcneg  16210  prmpwdvds  16240  prmreclem2  16253  4sqlem12  16292  vdwlem6  16322  vdwlem10  16326  vdwlem13  16329  0ram  16356  ram0  16358  ramz  16361  ramcl  16365  prmgaplem3  16389  prmgaplem4  16390  prmgaplem5  16391  prmgaplem6  16392  cshwshashlem1  16429  prmlem0  16439  firest  16706  imasaddfnlem  16801  imasvscafn  16810  mremre  16875  cicsym  17074  initoid  17265  termoid  17266  iszeroi  17269  drsdirfi  17548  pospo  17583  joinfval  17611  meetfval  17625  lubun  17733  odupos  17745  acsfiindd  17787  psss  17824  mnd1id  17953  0subm  17982  insubm  17983  sursubmefmnd  18061  injsubmefmnd  18062  smndex1mgm  18072  pwmnd  18102  dfgrp2e  18129  dfgrp3lem  18197  symgfix2  18544  f1omvdco2  18576  symggen  18598  odcau  18729  pgpfi  18730  sylow2blem3  18747  sylow3lem2  18753  lsmmod  18801  efgsfo  18865  frgpuptinv  18897  frgpnabllem1  18993  cyggeninv  19002  lt6abl  19015  cyggex2  19017  gsumval3lem2  19026  gsumval3  19027  gsum2d2  19094  dmdprdd  19121  dprd2da  19164  pgpfac1lem5  19201  pgpfac  19206  srgbinomlem4  19293  dvdsrtr  19402  dvdsrmul1  19403  lss1d  19735  lspsolvlem  19914  lspsnat  19917  lbsextlem2  19931  lbsextlem3  19932  0ring  20043  01eq0ring  20045  0ring01eqbi  20046  rng1nfld  20051  domnmuln0  20071  abvn0b  20075  mvrf1  20205  mplcoe5lem  20248  opsrtoslem2  20265  cply1mul  20462  coe1fzgsumdlem  20469  gsummoncoe1  20472  pf1ind  20518  evl1gsumdlem  20519  xrsdsreclblem  20591  qsssubdrg  20604  prmirredlem  20640  cygznlem3  20716  obslbs  20874  dsmmacl  20885  lindfrn  20965  lmiclbs  20981  lmisfree  20986  matecl  21034  mat1dimelbas  21080  scmateALT  21121  mdetdiaglem  21207  mdet0  21215  mdetunilem9  21229  gsummatr01  21268  cpmatmcllem  21326  m2cpminvid2lem  21362  pmatcollpw3fi1lem2  21395  chfacfscmul0  21466  chfacfpmmul0  21470  cayhamlem3  21495  tgcl  21577  tgidm  21588  indistopon  21609  fctop  21612  cctop  21614  ppttop  21615  pptbas  21616  epttop  21617  opnnei  21728  neiptopnei  21740  tgrest  21767  restntr  21790  perfopn  21793  ordtrest2lem  21811  isreg2  21985  lmmo  21988  ordthauslem  21991  cmpsublem  22007  cmpsub  22008  cmpcld  22010  hauscmplem  22014  iunconnlem  22035  unconn  22037  2ndcrest  22062  2ndcctbss  22063  2ndcdisj  22064  dis2ndc  22068  locfincmp  22134  comppfsc  22140  txbas  22175  ptbasin  22185  ptbasfi  22189  txcls  22212  txbasval  22214  ptpjopn  22220  ptclsg  22223  dfac14lem  22225  xkoccn  22227  txcnp  22228  txindis  22242  txdis1cn  22243  tx1stc  22258  tx2ndc  22259  txkgen  22260  xkoco1cn  22265  xkoco2cn  22266  xkococn  22268  xkoinjcn  22295  txconn  22297  fbfinnfr  22449  opnfbas  22450  filtop  22463  isfild  22466  fbunfip  22477  filconn  22491  fbasrn  22492  filuni  22493  isufil2  22516  filssufilg  22519  ufileu  22527  filufint  22528  rnelfmlem  22560  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem4  22565  fmfnfm  22566  hausflimi  22588  hauspwpwf1  22595  flffbas  22603  flftg  22604  alexsublem  22652  alexsubALTlem1  22655  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  alexsubALT  22659  ptcmplem3  22662  cldsubg  22719  qustgpopn  22728  tgptsmscld  22759  tsmsxplem1  22761  ustfilxp  22821  imasdsf1olem  22983  bldisj  23008  xbln0  23024  prdsxmslem2  23139  xrsblre  23419  icccmplem2  23431  reconn  23436  opnreen  23439  xrge0tsms  23442  metdsre  23461  iccpnfcnv  23548  cnheiborlem  23558  phtpc01  23600  pi1blem  23643  tcphcph  23840  cfilfcls  23877  iscau4  23882  bcthlem5  23931  bcth3  23934  cmssmscld  23953  hlhil  24046  ovolctb  24091  ovoliunlem2  24104  ovoliunnul  24108  ovolicc2  24123  volfiniun  24148  iundisj  24149  dyadmax  24199  dyadmbllem  24200  vitalilem2  24210  ismbfd  24240  mbfimaopnlem  24256  itg11  24292  i1faddlem  24294  mbfi1fseqlem4  24319  bddmulibl  24439  limciun  24492  perfdvf  24501  rolle  24587  dvivthlem1  24605  dvne0  24608  lhop1  24611  lhop2  24612  itgsubst  24646  dvdsq1p  24754  fta1g  24761  dgrco  24865  plydivex  24886  fta1  24897  ulmcaulem  24982  abelthlem2  25020  pilem2  25040  cxpmul2z  25274  cxpcn3lem  25328  xrlimcnp  25546  jensen  25566  wilthlem2  25646  wilthlem3  25647  muval2  25711  sqf11  25716  ppiublem1  25778  fsumvma  25789  lgsdir2lem2  25902  lgsdir2lem5  25905  lgsqrmodndvds  25929  gausslemma2dlem1a  25941  gausslemma2dlem3  25944  gausslemma2d  25950  2lgsoddprmlem2  25985  2sqreultlem  26023  2sqreunnltlem  26026  2sqreulem3  26029  dchrisum0fno1  26087  pntlem3  26185  pntleml  26187  ostthlem1  26203  ostth2lem2  26210  colinearalg  26696  axcontlem2  26751  axcontlem8  26757  edgupgr  26919  umgrpredgv  26925  numedglnl  26929  ausgrumgri  26952  ausgrusgri  26953  ushgredgedg  27011  ushgredgedgloop  27013  uhgr0v0e  27020  subumgredg2  27067  uhgrspansubgrlem  27072  uhgrspan1  27085  upgrreslem  27086  umgrreslem  27087  upgrres1  27095  fusgrfisstep  27111  nbuhgr  27125  nbuhgr2vtx1edgblem  27133  nbuhgr2vtx1edgb  27134  uhgrnbgr0nb  27136  edgnbusgreu  27149  nbusgredgeu0  27150  nbusgrf1o0  27151  nbusgrvtxm1uvtx  27187  cusgredg  27206  cusgrfi  27240  usgredgsscusgredg  27241  1loopgrnb0  27284  usgrvd0nedg  27315  uhgrvd00  27316  upgriswlk  27422  upgrwlkcompim  27424  uspgr2wlkeq  27427  uspgr2wlkeqi  27429  wlkv0  27432  wlklenvclwlkOLD  27437  wlkp1lem6  27460  lfgrwlkprop  27469  2pthnloop  27512  spthdep  27515  upgrwlkdvdelem  27517  usgr2wlkneq  27537  usgr2trlncl  27541  pthdlem1  27547  pthdlem2lem  27548  clwlkl1loop  27564  crctcshwlkn0lem3  27590  crctcshwlkn0lem5  27592  crctcshwlkn0  27599  0enwwlksnge1  27642  wlkiswwlks2  27653  wlkiswwlksupgr2  27655  wspthsnonn0vne  27696  umgr2adedgspth  27727  clwlkclwwlklem2a4  27775  clwlkclwwlklem2  27778  clwlkclwwlkf  27786  clwlkclwwlkfo  27787  erclwwlktr  27800  clwwlkf1  27828  erclwwlkntr  27850  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwwlknonex2e  27889  eucrctshift  28022  3cyclfrgrrn1  28064  frgrnbnb  28072  frgrncvvdeqlem2  28079  frgrncvvdeqlem3  28080  frgrncvvdeqlem9  28086  frgrwopreglem4a  28089  frgrwopregbsn  28096  frgrwopreg1  28097  frgrwopreg2  28098  frgrwopreglem5lem  28099  frgrwopreglem5ALT  28101  frgr2wwlk1  28108  numclwwlk1lem2foa  28133  numclwwlk1lem2f1  28136  wlkl0  28146  lnon0  28575  shmodsi  29166  shlub  29191  spanunsni  29356  h1datomi  29358  stm1ri  30021  stadd3i  30025  mdsl1i  30098  cvmdi  30101  superpos  30131  chjatom  30134  chirredi  30171  atcvat4i  30174  sumdmdii  30192  sumdmdlem  30195  cdj3lem2a  30213  cdj3lem3a  30216  cdj3i  30218  iunrnmptss  30317  disji2f  30327  disjif2  30331  iundisjf  30339  rnmposs  30419  iundisjfi  30519  nn0min  30536  wrdt2ind  30627  xrge0tsmsd  30692  cnre2csqima  31154  ordtrest2NEWlem  31165  xrge0iifcnv  31176  lmxrge0  31195  measdivcstALTV  31484  dya2iocuni  31541  omssubadd  31558  eulerpartlems  31618  bnj849  32197  bnj1118  32256  loop1cycl  32384  cusgracyclt3v  32403  derangenlem  32418  erdszelem9  32446  pconnconn  32478  iccllysconn  32497  cvmsval  32513  cvmscld  32520  cvmsss2  32521  cvmopnlem  32525  cvmfolem  32526  cvmliftmolem2  32529  cvmlift2lem10  32559  cvmlift2lem12  32561  cvmlift3lem5  32570  cvmlift3lem8  32573  satfdmlem  32615  satfrnmapom  32617  fmla1  32634  goalr  32644  fmlasucdisj  32646  satffunlem  32648  satffunlem1lem1  32649  satffunlem2lem1  32651  satffunlem2lem2  32653  msubvrs  32807  mthmblem  32827  untsucf  32936  3orel2  32941  3orel3  32942  nepss  32948  eqfunresadj  33004  dfon2lem5  33032  dfon2lem6  33033  dfon2lem7  33034  dfon2lem8  33035  rdgprc  33039  trpredtr  33069  dftrpred3g  33072  trpredrec  33077  frpomin  33078  frpoind  33080  frpoins2fg  33082  frmin  33084  frind  33085  frins2fg  33089  wzel  33111  wsuclem  33112  fpr3g  33122  frrlem9  33131  frrlem10  33132  frrlem12  33134  frrlem13  33135  nosepon  33172  noextendseq  33174  nolesgn2ores  33179  nosepdmlem  33187  nodenselem8  33195  noetalem3  33219  nocvxmin  33248  scutun12  33271  funpartfun  33404  altopth1  33426  altopth2  33427  colineardim1  33522  lineext  33537  btwnconn1lem14  33561  brsegle  33569  hilbert1.2  33616  trer  33664  elicc3  33665  finminlem  33666  fneint  33696  fnessref  33705  refssfne  33706  neibastop1  33707  neibastop2lem  33708  neibastop2  33709  fnemeet2  33715  fnejoin2  33717  tailfb  33725  arg-ax  33764  ordtoplem  33783  onsuct0  33789  bj-gl4  33929  bj-nfimt  33971  bj-nnfim  34075  bj-nnfor  34079  bj-nnford  34080  bj-nnflemee  34092  bj-19.36im  34100  bj-19.37im  34101  bj-sngltag  34298  bj-restn0  34384  bj-0int  34396  bj-ismooredr2  34405  bj-bary1lem1  34595  icorempo  34635  icoreresf  34636  relowlssretop  34647  rdgssun  34662  exrecfnlem  34663  finxpreclem6  34680  pibt2  34701  fin2so  34894  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  mblfinlem1  34944  mblfinlem4  34947  ovoliunnfl  34949  itg2addnclem  34958  itg2addnclem2  34959  areacirc  35002  unirep  35003  filbcmb  35030  sdclem1  35033  fdc  35035  nninfnub  35041  isbnd2  35076  ssbnd  35081  prdsbnd2  35088  cntotbnd  35089  heibor1lem  35102  heiborlem1  35104  heiborlem4  35107  heiborlem6  35109  0idl  35318  intidl  35322  unichnidl  35324  keridl  35325  prnc  35360  iss2  35616  eqvreldisj  35864  erim  35927  prtlem17  36027  prter2  36032  ax12indn  36094  lsatn0  36150  lsatcmp  36154  lssat  36167  lfl1  36221  lshpsmreu  36260  lkrin  36315  glbconxN  36529  cvrat4  36594  paddasslem17  36987  pmodlem2  36998  dalawlem14  37035  pclclN  37042  pclfinN  37051  pclfinclN  37101  poml4N  37104  osumcllem8N  37114  pexmidlem5N  37125  cdleme32a  37592  cdlemg33b0  37852  tendoeq2  37925  diaelrnN  38196  dihmeetlem1N  38441  dihglblem5apreN  38442  dihglblem2N  38445  dochvalr  38508  dochkrshp  38537  lcfl6  38651  lcfrvalsnN  38692  mapdordlem2  38788  mapdh8b  38931  mapdh9a  38940  hdmap14lem13  39031  nn0expgcd  39233  3cubes  39336  eldioph2b  39409  eldiophss  39420  diophren  39459  ctbnfien  39464  rencldnfilem  39466  pellexlem3  39477  pellexlem5  39479  pellex  39481  pell14qrexpcl  39513  pellfundre  39527  pellfundge  39528  pellfundlb  39530  pellfundglb  39531  jm2.19lem4  39638  fnwe2lem2  39700  pwssplit4  39738  hbtlem5  39777  ss2iundf  40053  relexpmulg  40104  relexpxpmin  40111  relexpaddss  40112  dftrcl3  40114  dfrtrcl3  40127  clsk1indlem3  40442  isotone1  40447  isotone2  40448  ntrneiel2  40485  ntrneik4w  40499  rexlimdvaacbv  40607  rexlimddvcbvw  40608  onfrALT  40932  ax6e2ndeq  40942  snssiALT  41211  iinssf  41456  hirstL-ax3  43177  euoreqb  43357  2reu8i  43361  otiunsndisjX  43527  f1oresf1o2  43539  subsubelfzo0  43575  iccpartiltu  43631  iccpartigtl  43632  iccpartltu  43634  ichnfim  43673  ichnreuop  43683  ichreuopeq  43684  sprsymrelf1lem  43702  sprsymrelfolem2  43704  sprsymrelf1  43707  sprsymrelfo  43708  prproropf1olem2  43715  prproropf1olem4  43717  paireqne  43722  reuopreuprim  43737  fmtnofac2lem  43779  fmtno4prmfac  43783  prmdvdsfmtnof1lem1  43795  lighneallem2  43820  opoeALTV  43897  opeoALTV  43898  even3prm2  43933  fpprel2  43955  gbegt5  43975  gbowgt5  43976  sbgoldbwt  43991  sbgoldbst  43992  sbgoldbalt  43995  sbgoldbm  43998  mogoldbb  43999  sbgoldbo  44001  nnsum3primesle9  44008  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  wtgoldbnnsum4prm  44016  bgoldbnnsum3prm  44018  bgoldbtbndlem1  44019  bgoldbtbndlem4  44022  bgoldbtbnd  44023  isomushgr  44040  isomuspgrlem2b  44043  isomuspgrlem2c  44044  upgrwlkupwlk  44064  mgmpropd  44091  copisnmnd  44125  mgm2mgm  44183  ringrng  44199  c0snmgmhm  44234  ztprmneprm  44444  mndpsuppss  44468  lindslinindimp2lem4  44565  lindslinindsimp2  44567  lindsrng01  44572  snlindsntor  44575  ldepspr  44577  isldepslvec2  44589  suppdm  44614  blen1b  44697  dignn0ldlem  44711  digexp  44716  nn0sumshdiglemB  44729  nn0sumshdiglem1  44730  prelrrx2b  44750  eenglngeehlnmlem1  44773  line2ylem  44787  line2xlem  44789  itschlc0xyqsol1  44802  itschlc0xyqsol  44803  itsclc0  44807  2itscp  44817  inlinecirc02plem  44822  iunord  44828  tfis2d  44832