Theorem biimtrid 241

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
biimtrid.1	⊢ (𝜑 ↔ 𝜓)
biimtrid.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

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

Proof of Theorem biimtrid

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr4g  295  3orel1  1091  3orel2  1485  3orel3  1486  cad0  1619  ax13  2373  2euexv  2626  2euex  2636  eqneqall  2950  necon3bd  2953  pm2.24nel  3058  spcimgft  3547  rspc  3570  rspcimdv  3572  rspc2gv  3590  euind  3685  reuind  3714  2reurex  3721  sbciegft  3780  rspsbc  3838  elneeldif  3927  ssexnelpss  4078  rspn0  4317  ralnralall  4481  pwpw0  4778  sssn  4791  prnebg  4818  pwsnOLD  4863  intss1  4929  intmin  4934  uniintsn  4953  iinss  5021  iinss2  5022  disji2  5092  disjiun  5097  disjiund  5100  disjxiun  5107  trel3  5237  trin  5239  eusvnfb  5353  reusv3  5365  axprlem2  5384  copsexgw  5452  copsexg  5453  propeqop  5469  otiunsndisj  5482  iunopeqop  5483  po3nr  5565  friOLD  5599  wefrc  5632  wereu2  5635  ssrelrel  5757  relop  5811  iss  5994  poirr2  6083  xpcan  6133  xpcan2  6134  sossfld  6143  frpomin  6299  frpoind  6301  frpoins2fg  6303  wfiOLD  6310  wfis2fgOLD  6316  onfr  6361  onmindif  6414  onun2  6430  iotan0  6491  funopg  6540  funssres  6550  funun  6552  fv3  6865  fvmptt  6973  iinpreima  7024  fvn0ssdmfun  7030  dff3  7055  dff4  7056  fmptsng  7119  fmptsnd  7120  tpres  7155  fnprb  7163  fntpb  7164  fvclss  7194  fpropnf1  7219  isomin  7287  isofrlem  7290  weniso  7304  eqfunresadj  7310  oprabidw  7393  oprabid  7394  ssorduni  7718  onmindif2  7747  limuni3  7793  tfis2f  7797  tfinds  7801  tfinds2  7805  tfinds3  7806  funcnvuni  7873  f1oweALT  7910  funeldmdif  7985  f1o2ndf1  8059  poxp  8065  soxp  8066  fnse  8070  frpoins3xpg  8077  frpoins3xp3g  8078  xpord2pred  8082  sexp2  8083  poxp3  8087  xpord3pred  8089  sexp3  8090  xpord3inddlem  8091  suppimacnv  8110  suppcoss  8143  mpoxopynvov0g  8150  reldmtpos  8170  rntpos  8175  fpr3g  8221  frrlem9  8230  frrlem10  8231  frrlem12  8233  frrlem13  8234  wfrlem14OLD  8273  wfrlem15OLD  8274  onfununi  8292  smoiun  8312  tfrlem1  8327  tfr3  8350  frsucmptn  8390  tz7.49  8396  oaordi  8498  oawordeulem  8506  omeulem1  8534  oeordi  8539  oelimcl  8552  nnaordi  8570  nneob  8607  omsmolem  8608  naddssim  8636  erdisj  8707  qsss  8724  uniinqs  8743  fsetfcdm  8805  map0g  8829  resixpfo  8881  ixpsnf1o  8883  xpdom3  9021  mapdom3  9100  ssfiALT  9125  phplem2  9159  php3  9163  phplem4OLD  9171  php3OLD  9175  0sdom1dom  9189  sdom1  9193  unxpdomlem3  9203  findcard2OLD  9235  findcard3  9236  findcard3OLD  9237  frfi  9239  isfiniteg  9255  xpfiOLD  9269  fiint  9275  finsschain  9310  dffi2  9368  marypha1lem  9378  marypha2  9384  supmo  9397  suplub2  9406  infmo  9440  ordiso2  9460  ordtypelem7  9469  ordtypelem8  9470  brwdom2  9518  unxpwdom2  9533  ixpiunwdom  9535  elirrv  9541  suc11reg  9564  noinfep  9605  cantnfle  9616  cantnflem1  9634  cantnf  9638  trcl  9673  epfrs  9676  frmin  9694  frind  9695  frins2f  9698  rankpwi  9768  rankunb  9795  rankuni2b  9798  rankxplim3  9826  cplem1  9834  karden  9840  carddom2  9922  fseqenlem2  9970  ac10ct  9979  acni2  9991  acndom  9996  infpwfien  10007  alephordi  10019  alephord  10020  iunfictbso  10059  aceq3lem  10065  dfac5  10073  dfac2b  10075  dfac12lem3  10090  dfac12r  10091  cdainflem  10132  cfub  10194  cfeq0  10201  coflim  10206  cfslb2n  10213  cofsmo  10214  coftr  10218  infpssr  10253  fin23lem7  10261  fin23lem11  10262  fin23lem21  10284  isf32lem2  10299  isf34lem4  10322  isfin1-2  10330  isfin1-3  10331  fin1a2lem9  10353  fin1a2lem11  10355  fin1a2lem12  10356  fin1a2lem13  10357  domtriomlem  10387  axdc3lem2  10396  axcclem  10402  ac6c4  10426  zorn2lem4  10444  zorn2lem5  10445  zorn2lem7  10447  ttukeylem5  10458  ttukeyg  10462  brdom6disj  10477  fnrndomg  10481  iunfo  10484  iundom2g  10485  ficard  10510  konigthlem  10513  alephval2  10517  pwcfsdom  10528  fpwwe2lem8  10583  fpwwe2lem10  10585  fpwwe2lem11  10586  fpwwe2lem12  10587  pwfseqlem3  10605  gchpwdom  10615  winalim2  10641  gchina  10644  wunex2  10683  tskr1om2  10713  tskxpss  10717  inar1  10720  tskuni  10728  gruun  10751  grudomon  10762  grur1  10765  ltmpi  10849  ltexprlem2  10982  ltexprlem6  10986  reclem2pr  10993  reclem3pr  10994  reclem4pr  10995  suplem1pr  10997  mulgt0sr  11050  supsrlem  11056  axrrecex  11108  axpre-sup  11114  ltlen  11265  addid0  11583  negn0  11593  negf1o  11594  mulge0b  12034  supaddc  12131  supadd  12132  supmul1  12133  supmullem1  12134  supmullem2  12135  supmul  12136  cju  12158  nnsub  12206  0mnnnnn0  12454  un0addcl  12455  un0mulcl  12456  nn0sub  12472  nn0n0n1ge2b  12490  zle0orge1  12525  peano5uzi  12601  eluzuzle  12781  zsupss  12871  elpq  12909  qbtwnre  13128  xrsupexmnf  13234  xrinfmexpnf  13235  xrsupsslem  13236  xrinfmsslem  13237  xrub  13241  supxrun  13245  ixxdisj  13289  icodisj  13403  difreicc  13411  uzsubsubfz  13473  fzadd2  13486  elfzmlbp  13562  fzofzim  13629  elfznelfzo  13687  injresinj  13703  subfzo0  13704  flval3  13730  modirr  13857  modsumfzodifsn  13859  addmodlteq  13861  ssnn0fi  13900  seqf1o  13959  expcl2lem  13989  expnegz  14012  expaddz  14022  expmulz  14024  facwordi  14199  faclbnd4lem4  14206  bccl  14232  hashnfinnn0  14271  hashgt12el  14332  hashgt12el2  14333  hashfun  14347  hashbclem  14361  hashbc  14362  hashfacen  14363  hashfacenOLD  14364  hashf1lem1  14365  hashf1lem1OLD  14366  hashf1  14368  hash2pwpr  14387  fundmge2nop0  14403  fi1uzind  14408  brfi1indALT  14411  swrdnd0  14557  wrdind  14622  wrd2ind  14623  swrdccatin1  14625  swrdccatin2  14629  pfxccat3  14634  pfxccat3a  14638  swrdccat3blem  14639  reuccatpfxs1  14647  cshw1  14722  cshwcsh2id  14729  wwlktovfo  14859  s3iunsndisj  14865  rtrclreclem3  14957  dfrtrcl2  14959  01sqrexlem1  15139  01sqrexlem6  15144  rexanre  15243  cau3lem  15251  2clim  15466  summo  15613  fsum2dlem  15666  fsumiun  15717  prodmo  15830  fprod2dlem  15874  bpolycl  15946  rpnnen2lem12  16118  odd2np1lem  16233  oddge22np1  16242  sqoddm1div8z  16247  sumeven  16280  pwp1fsum  16284  bitsfzo  16326  sadcaddlem  16348  gcd0id  16410  algcvgblem  16464  lcmfunsnlem1  16524  lcmfunsnlem2lem1  16525  lcmfunsnlem2  16527  coprmproddvdslem  16549  divgcdcoprm0  16552  isprm7  16595  prmdvdsexpr  16604  prmfac1  16608  qnumdencl  16625  hashdvds  16658  prm23lt5  16697  pcneg  16757  prmpwdvds  16787  prmreclem2  16800  4sqlem12  16839  vdwlem6  16869  vdwlem10  16873  vdwlem13  16876  0ram  16903  ram0  16905  ramz  16908  ramcl  16912  prmgaplem3  16936  prmgaplem4  16937  prmgaplem5  16938  prmgaplem6  16939  cshwshashlem1  16979  prmlem0  16989  firest  17328  imasaddfnlem  17424  imasvscafn  17433  mremre  17498  cicsym  17701  initoid  17901  termoid  17902  iszeroi  17909  drsdirfi  18208  odupos  18231  pospo  18248  joinfval  18276  meetfval  18290  lubun  18418  acsfiindd  18456  psss  18483  mnd1id  18612  0subm  18642  insubm  18643  sursubmefmnd  18720  injsubmefmnd  18721  smndex1mgm  18731  pwmnd  18761  dfgrp2e  18790  dfgrp3lem  18859  symgfix2  19212  f1omvdco2  19244  symggen  19266  odcau  19400  pgpfi  19401  sylow2blem3  19418  sylow3lem2  19424  lsmmod  19471  efgsfo  19535  frgpuptinv  19567  frgpnabllem1  19665  cyggeninv  19674  lt6abl  19686  cyggex2  19688  gsumval3lem2  19697  gsumval3  19698  gsum2d2  19765  dmdprdd  19792  dprd2da  19835  pgpfac1lem5  19872  pgpfac  19877  srgbinomlem4  19974  dvdsrtr  20095  dvdsrmul1  20096  0ring  20213  01eq0ringOLD  20216  0ring01eqbi  20217  lss1d  20481  lspsolvlem  20662  lspsnat  20665  lbsextlem2  20679  lbsextlem3  20680  domnmuln0  20805  abvn0b  20809  xrsdsreclblem  20880  qsssubdrg  20893  prmirredlem  20930  cygznlem3  21013  obslbs  21173  dsmmacl  21184  lindfrn  21264  lmiclbs  21280  lmisfree  21285  mvrf1  21431  mplcoe5lem  21477  opsrtoslem2  21500  cply1mul  21702  coe1fzgsumdlem  21709  gsummoncoe1  21712  pf1ind  21758  evl1gsumdlem  21759  matecl  21811  mat1dimelbas  21857  scmateALT  21898  mdetdiaglem  21984  mdet0  21992  mdetunilem9  22006  gsummatr01  22045  cpmatmcllem  22104  m2cpminvid2lem  22140  pmatcollpw3fi1lem2  22173  chfacfscmul0  22244  chfacfpmmul0  22248  cayhamlem3  22273  tgcl  22356  tgidm  22367  indistopon  22388  fctop  22391  cctop  22393  ppttop  22394  pptbas  22395  epttop  22396  opnnei  22508  neiptopnei  22520  tgrest  22547  restntr  22570  perfopn  22573  ordtrest2lem  22591  isreg2  22765  lmmo  22768  ordthauslem  22771  cmpsublem  22787  cmpsub  22788  cmpcld  22790  hauscmplem  22794  iunconnlem  22815  unconn  22817  2ndcrest  22842  2ndcctbss  22843  2ndcdisj  22844  dis2ndc  22848  locfincmp  22914  comppfsc  22920  txbas  22955  ptbasin  22965  ptbasfi  22969  txcls  22992  txbasval  22994  ptpjopn  23000  ptclsg  23003  dfac14lem  23005  xkoccn  23007  txcnp  23008  txindis  23022  txdis1cn  23023  tx1stc  23038  tx2ndc  23039  txkgen  23040  xkoco1cn  23045  xkoco2cn  23046  xkococn  23048  xkoinjcn  23075  txconn  23077  fbfinnfr  23229  opnfbas  23230  filtop  23243  isfild  23246  fbunfip  23257  filconn  23271  fbasrn  23272  filuni  23273  isufil2  23296  filssufilg  23299  ufileu  23307  filufint  23308  rnelfmlem  23340  rnelfm  23341  fmfnfmlem2  23343  fmfnfmlem4  23345  fmfnfm  23346  hausflimi  23368  hauspwpwf1  23375  flffbas  23383  flftg  23384  alexsublem  23432  alexsubALTlem1  23435  alexsubALTlem2  23436  alexsubALTlem3  23437  alexsubALTlem4  23438  alexsubALT  23439  ptcmplem3  23442  cldsubg  23499  qustgpopn  23508  tgptsmscld  23539  tsmsxplem1  23541  ustfilxp  23601  imasdsf1olem  23763  bldisj  23788  xbln0  23804  prdsxmslem2  23922  xrsblre  24211  icccmplem2  24223  reconn  24228  opnreen  24231  xrge0tsms  24234  metdsre  24253  iccpnfcnv  24344  cnheiborlem  24354  phtpc01  24396  pi1blem  24439  tcphcph  24638  cfilfcls  24675  iscau4  24680  bcthlem5  24729  bcth3  24732  cmssmscld  24751  hlhil  24844  ovolctb  24891  ovoliunlem2  24904  ovoliunnul  24908  ovolicc2  24923  volfiniun  24948  iundisj  24949  dyadmax  24999  dyadmbllem  25000  vitalilem2  25010  ismbfd  25040  mbfimaopnlem  25056  itg11  25092  i1faddlem  25094  mbfi1fseqlem4  25120  bddmulibl  25240  limciun  25295  perfdvf  25304  rolle  25391  dvivthlem1  25409  dvne0  25412  lhop1  25415  lhop2  25416  itgsubst  25450  dvdsq1p  25562  fta1g  25569  dgrco  25673  plydivex  25694  fta1  25705  ulmcaulem  25790  abelthlem2  25828  pilem2  25848  cxpmul2z  26083  cxpcn3lem  26137  xrlimcnp  26355  jensen  26375  wilthlem2  26455  wilthlem3  26456  muval2  26520  sqf11  26525  ppiublem1  26587  fsumvma  26598  lgsdir2lem2  26711  lgsdir2lem5  26714  lgsqrmodndvds  26738  gausslemma2dlem1a  26750  gausslemma2dlem3  26753  gausslemma2d  26759  2lgsoddprmlem2  26794  2sqreultlem  26832  2sqreunnltlem  26835  2sqreulem3  26838  dchrisum0fno1  26896  pntlem3  26994  pntleml  26996  ostthlem1  27012  ostth2lem2  27019  nosepon  27050  noextendseq  27052  nolesgn2ores  27057  nogesgn1ores  27059  nosepdmlem  27068  nodenselem8  27076  noinfno  27103  noetasuplem4  27121  nocvxmin  27161  scutun12  27192  madebdayim  27260  sltlpss  27279  addsproplem2  27325  sleadd1  27341  addsunif  27353  negsproplem2  27370  negsid  27382  negsunif  27393  mulsproplem10  27431  colinearalg  27922  axcontlem2  27977  axcontlem8  27983  edgupgr  28148  umgrpredgv  28154  numedglnl  28158  ausgrumgri  28181  ausgrusgri  28182  ushgredgedg  28240  ushgredgedgloop  28242  uhgr0v0e  28249  subumgredg2  28296  uhgrspansubgrlem  28301  uhgrspan1  28314  upgrreslem  28315  umgrreslem  28316  upgrres1  28324  fusgrfisstep  28340  nbuhgr  28354  nbuhgr2vtx1edgblem  28362  nbuhgr2vtx1edgb  28363  uhgrnbgr0nb  28365  edgnbusgreu  28378  nbusgredgeu0  28379  nbusgrf1o0  28380  nbusgrvtxm1uvtx  28416  cusgredg  28435  cusgrfi  28469  usgredgsscusgredg  28470  1loopgrnb0  28513  usgrvd0nedg  28544  uhgrvd00  28545  upgriswlk  28652  upgrwlkcompim  28654  uspgr2wlkeq  28657  uspgr2wlkeqi  28659  wlkv0  28662  wlkp1lem6  28689  lfgrwlkprop  28698  2pthnloop  28742  spthdep  28745  upgrwlkdvdelem  28747  usgr2wlkneq  28767  usgr2trlncl  28771  pthdlem1  28777  pthdlem2lem  28778  clwlkl1loop  28794  crctcshwlkn0lem3  28820  crctcshwlkn0lem5  28822  crctcshwlkn0  28829  0enwwlksnge1  28872  wlkiswwlks2  28883  wlkiswwlksupgr2  28885  wspthsnonn0vne  28925  umgr2adedgspth  28956  clwlkclwwlklem2a4  29004  clwlkclwwlklem2  29007  clwlkclwwlkf  29015  clwlkclwwlkfo  29016  erclwwlktr  29029  clwwlkf1  29056  erclwwlkntr  29078  hashecclwwlkn1  29084  umgrhashecclwwlk  29085  clwwlknonex2e  29117  eucrctshift  29250  3cyclfrgrrn1  29292  frgrnbnb  29300  frgrncvvdeqlem2  29307  frgrncvvdeqlem3  29308  frgrncvvdeqlem9  29314  frgrwopreglem4a  29317  frgrwopregbsn  29324  frgrwopreg1  29325  frgrwopreg2  29326  frgrwopreglem5lem  29327  frgrwopreglem5ALT  29329  frgr2wwlk1  29336  numclwwlk1lem2foa  29361  numclwwlk1lem2f1  29364  wlkl0  29374  lnon0  29803  shmodsi  30394  shlub  30419  spanunsni  30584  h1datomi  30586  stm1ri  31249  stadd3i  31253  mdsl1i  31326  cvmdi  31329  superpos  31359  chjatom  31362  chirredi  31399  atcvat4i  31402  sumdmdii  31420  sumdmdlem  31423  cdj3lem2a  31441  cdj3lem3a  31444  cdj3i  31446  iunrnmptss  31551  disji2f  31562  disjif2  31566  iundisjf  31574  rnmposs  31657  iundisjfi  31767  nn0min  31786  wrdt2ind  31877  xrge0tsmsd  31969  cnre2csqima  32581  ordtrest2NEWlem  32592  xrge0iifcnv  32603  lmxrge0  32622  measdivcstALTV  32913  dya2iocuni  32972  omssubadd  32989  eulerpartlems  33049  bnj849  33626  bnj1118  33685  loop1cycl  33818  cusgracyclt3v  33837  derangenlem  33852  erdszelem9  33880  pconnconn  33912  iccllysconn  33931  cvmsval  33947  cvmscld  33954  cvmsss2  33955  cvmopnlem  33959  cvmfolem  33960  cvmliftmolem2  33963  cvmlift2lem10  33993  cvmlift2lem12  33995  cvmlift3lem5  34004  cvmlift3lem8  34007  satfdmlem  34049  satfrnmapom  34051  fmla1  34068  goalr  34078  fmlasucdisj  34080  satffunlem  34082  satffunlem1lem1  34083  satffunlem2lem1  34085  satffunlem2lem2  34087  msubvrs  34241  mthmblem  34261  untsucf  34368  nepss  34376  dfon2lem5  34448  dfon2lem6  34449  dfon2lem7  34450  dfon2lem8  34451  rdgprc  34455  wzel  34485  wsuclem  34486  funpartfun  34604  altopth1  34626  altopth2  34627  colineardim1  34722  lineext  34737  btwnconn1lem14  34761  brsegle  34769  hilbert1.2  34816  trer  34864  elicc3  34865  finminlem  34866  fneint  34896  fnessref  34905  refssfne  34906  neibastop1  34907  neibastop2lem  34908  neibastop2  34909  fnemeet2  34915  fnejoin2  34917  tailfb  34925  arg-ax  34964  ordtoplem  34983  onsuct0  34989  bj-gl4  35136  bj-nfimt  35178  bj-nnfim  35287  bj-nnfor  35291  bj-nnford  35292  bj-nnflemee  35304  bj-19.36im  35312  bj-19.37im  35313  bj-sngltag  35527  bj-restn0  35634  bj-0int  35645  bj-ismooredr2  35654  bj-bary1lem1  35855  icorempo  35895  icoreresf  35896  relowlssretop  35907  rdgssun  35922  exrecfnlem  35923  finxpreclem6  35940  pibt2  35961  fin2so  36138  poimirlem24  36175  poimirlem25  36176  poimirlem26  36177  poimirlem27  36178  poimirlem29  36180  poimirlem30  36181  poimirlem31  36182  mblfinlem1  36188  mblfinlem4  36191  ovoliunnfl  36193  itg2addnclem  36202  itg2addnclem2  36203  areacirc  36244  unirep  36245  filbcmb  36272  sdclem1  36275  fdc  36277  nninfnub  36283  isbnd2  36315  ssbnd  36320  prdsbnd2  36327  cntotbnd  36328  heibor1lem  36341  heiborlem1  36343  heiborlem4  36346  heiborlem6  36348  0idl  36557  intidl  36561  unichnidl  36563  keridl  36564  prnc  36599  iss2  36878  mopickr  36897  refressn  36978  eqvreldisj  37149  erimeq  37214  disjlem17  37334  eldisjlem19  37345  prtlem17  37411  prter2  37416  ax12indn  37478  lsatn0  37534  lsatcmp  37538  lssat  37551  lfl1  37605  lshpsmreu  37644  lkrin  37699  glbconxN  37914  cvrat4  37979  paddasslem17  38372  pmodlem2  38383  dalawlem14  38420  pclclN  38427  pclfinN  38436  pclfinclN  38486  poml4N  38489  osumcllem8N  38499  pexmidlem5N  38510  cdleme32a  38977  cdlemg33b0  39237  tendoeq2  39310  diaelrnN  39581  dihmeetlem1N  39826  dihglblem5apreN  39827  dihglblem2N  39830  dochvalr  39893  dochkrshp  39922  lcfl6  40036  lcfrvalsnN  40077  mapdordlem2  40173  mapdh8b  40316  mapdh9a  40325  hdmap14lem13  40416  fsuppind  40823  nn0expgcd  40879  nna4b4nsq  41056  3cubes  41071  eldioph2b  41144  eldiophss  41155  diophren  41194  ctbnfien  41199  rencldnfilem  41201  pellexlem3  41212  pellexlem5  41214  pellex  41216  pell14qrexpcl  41248  pellfundre  41262  pellfundge  41263  pellfundlb  41265  pellfundglb  41266  jm2.19lem4  41374  fnwe2lem2  41436  pwssplit4  41474  hbtlem5  41513  cantnfresb  41717  naddwordnexlem4  41795  safesnsupfiss  41809  ss2iundf  42053  relexpmulg  42104  relexpxpmin  42111  relexpaddss  42112  dftrcl3  42114  dfrtrcl3  42127  clsk1indlem3  42437  isotone1  42442  isotone2  42443  ntrneiel2  42480  ntrneik4w  42494  rexlimdvaacbv  42600  rexlimddvcbvw  42601  ismnushort  42703  onfrALT  42953  ax6e2ndeq  42963  snssiALT  43232  iinssf  43470  hirstL-ax3  45247  fsetsnfo  45407  cfsetsnfsetf1  45413  cfsetsnfsetfo  45414  fcoresf1  45423  euoreqb  45461  2reu8i  45465  otiunsndisjX  45631  f1oresf1o2  45643  subsubelfzo0  45678  iccpartiltu  45734  iccpartigtl  45735  iccpartltu  45737  ichnfim  45776  ichnreuop  45784  ichreuopeq  45785  sprsymrelf1lem  45803  sprsymrelfolem2  45805  sprsymrelf1  45808  sprsymrelfo  45809  prproropf1olem2  45816  prproropf1olem4  45818  paireqne  45823  reuopreuprim  45838  fmtnofac2lem  45880  fmtno4prmfac  45884  prmdvdsfmtnof1lem1  45896  lighneallem2  45918  opoeALTV  45995  opeoALTV  45996  even3prm2  46031  fpprel2  46053  gbegt5  46073  gbowgt5  46074  sbgoldbwt  46089  sbgoldbst  46090  sbgoldbalt  46093  sbgoldbm  46096  mogoldbb  46097  sbgoldbo  46099  nnsum3primesle9  46106  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  wtgoldbnnsum4prm  46114  bgoldbnnsum3prm  46116  bgoldbtbndlem1  46117  bgoldbtbndlem4  46120  bgoldbtbnd  46121  isomushgr  46138  isomuspgrlem2b  46141  isomuspgrlem2c  46142  upgrwlkupwlk  46162  mgmpropd  46189  copisnmnd  46223  mgm2mgm  46281  ringrng  46297  c0snmgmhm  46332  ztprmneprm  46543  mndpsuppss  46567  lindslinindimp2lem4  46662  lindslinindsimp2  46664  lindsrng01  46669  snlindsntor  46672  ldepspr  46674  isldepslvec2  46686  suppdm  46711  blen1b  46794  dignn0ldlem  46808  digexp  46813  nn0sumshdiglemB  46826  nn0sumshdiglem1  46827  prelrrx2b  46920  eenglngeehlnmlem1  46943  line2ylem  46957  line2xlem  46959  itschlc0xyqsol1  46972  itschlc0xyqsol  46973  itsclc0  46977  2itscp  46987  inlinecirc02plem  46992  opnneilv  47061  iunord  47241  tfis2d  47245