Theorem biimtrid 242

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 216	. 2 ⊢ (𝜑 → 𝜓)
3		biimtrid.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	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:  3imtr4g  296  3orel1  1091  3orel2  1486  3orel2OLD  1487  3orel3  1488  cad0  1618  ax12ev2  2180  ax13  2380  2euexv  2631  2euex  2641  eqneqall  2951  necon3bd  2954  pm2.24nel  3059  spcimgfi1OLD  3548  rspc  3610  rspcimdv  3612  rspc2gv  3632  euind  3730  reuind  3759  2reurex  3766  sbciegftOLD  3826  sbccomlem  3869  rspsbc  3879  elneeldif  3965  ssexnelpss  4116  rspn0  4356  ralnralall  4515  pwpw0  4813  sssn  4826  prnebg  4856  intss1  4963  intmin  4968  uniintsn  4985  iinss  5056  iinss2  5057  disji2  5127  disjiun  5131  disjiund  5134  disjxiun  5140  trel3  5269  trin  5271  eusvnfb  5393  reusv3  5405  axprlem2  5424  copsexgw  5495  copsexg  5496  propeqop  5512  otiunsndisj  5525  iunopeqop  5526  po3nr  5607  friOLD  5643  wefrc  5679  wereu2  5682  ssrelrel  5806  relop  5861  iss  6053  poirr2  6144  imadifssran  6171  xpcan  6196  xpcan2  6197  sossfld  6206  frpomin  6361  frpoind  6363  frpoins2fg  6365  wfiOLD  6372  wfis2fgOLD  6378  onfr  6423  onmindif  6476  onun2  6492  iotan0  6551  funopg  6600  funssres  6610  funun  6612  fv3  6924  fvmptt  7036  iinpreima  7089  fvn0ssdmfun  7094  dff3  7120  dff4  7121  fmptsng  7188  fmptsnd  7189  tpres  7221  fnprb  7228  fntpb  7229  fvclss  7261  fpropnf1  7287  isomin  7357  isofrlem  7360  weniso  7374  eqfunresadj  7380  oprabidw  7462  oprabid  7463  ssorduni  7799  onmindif2  7827  limuni3  7873  tfis2f  7877  tfinds  7881  tfinds2  7885  tfinds3  7886  omun  7909  funcnvuni  7954  resf1extb  7956  f1oweALT  7997  funeldmdif  8073  f1o2ndf1  8147  poxp  8153  soxp  8154  fnse  8158  frpoins3xpg  8165  frpoins3xp3g  8166  xpord2pred  8170  sexp2  8171  poxp3  8175  xpord3pred  8177  sexp3  8178  xpord3inddlem  8179  suppimacnv  8199  suppcoss  8232  mpoxopynvov0g  8239  reldmtpos  8259  rntpos  8264  fpr3g  8310  frrlem9  8319  frrlem10  8320  frrlem12  8322  frrlem13  8323  wfrlem14OLD  8362  wfrlem15OLD  8363  onfununi  8381  smoiun  8401  tfrlem1  8416  tfr3  8439  frsucmptn  8479  tz7.49  8485  oaordi  8584  oawordeulem  8592  omeulem1  8620  oeordi  8625  oelimcl  8638  nnaordi  8656  nneob  8694  omsmolem  8695  naddssim  8723  erdisj  8799  qsss  8818  uniinqs  8837  fsetfcdm  8900  map0g  8924  resixpfo  8976  ixpsnf1o  8978  xpdom3  9110  mapdom3  9189  ssfiALT  9214  phplem2  9245  php3  9249  phplem4OLD  9257  php3OLD  9261  0sdom1dom  9274  sdom1  9278  unxpdomlem3  9288  findcard3  9318  findcard3OLD  9319  frfi  9321  isfiniteg  9337  xpfiOLD  9359  fiint  9366  fiintOLD  9367  finsschain  9399  dffi2  9463  marypha1lem  9473  marypha2  9479  supmo  9492  suplub2  9501  infmo  9535  ordiso2  9555  ordtypelem7  9564  ordtypelem8  9565  brwdom2  9613  unxpwdom2  9628  ixpiunwdom  9630  elirrv  9636  suc11reg  9659  noinfep  9700  cantnfle  9711  cantnflem1  9729  cantnf  9733  trcl  9768  epfrs  9771  frmin  9789  frind  9790  frins2f  9793  rankpwi  9863  rankunb  9890  rankuni2b  9893  rankxplim3  9921  cplem1  9929  karden  9935  carddom2  10017  fseqenlem2  10065  ac10ct  10074  acni2  10086  acndom  10091  infpwfien  10102  alephordi  10114  alephord  10115  iunfictbso  10154  aceq3lem  10160  dfac5  10169  dfac2b  10171  dfac12lem3  10186  dfac12r  10187  cdainflem  10228  cfub  10289  cfeq0  10296  coflim  10301  cfslb2n  10308  cofsmo  10309  coftr  10313  infpssr  10348  fin23lem7  10356  fin23lem11  10357  fin23lem21  10379  isf32lem2  10394  isf34lem4  10417  isfin1-2  10425  isfin1-3  10426  fin1a2lem9  10448  fin1a2lem11  10450  fin1a2lem12  10451  fin1a2lem13  10452  domtriomlem  10482  axdc3lem2  10491  axcclem  10497  ac6c4  10521  zorn2lem4  10539  zorn2lem5  10540  zorn2lem7  10542  ttukeylem5  10553  ttukeyg  10557  brdom6disj  10572  fnrndomg  10576  iunfo  10579  iundom2g  10580  ficard  10605  konigthlem  10608  alephval2  10612  pwcfsdom  10623  fpwwe2lem8  10678  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2lem12  10682  pwfseqlem3  10700  gchpwdom  10710  winalim2  10736  gchina  10739  wunex2  10778  tskr1om2  10808  tskxpss  10812  inar1  10815  tskuni  10823  gruun  10846  grudomon  10857  grur1  10860  ltmpi  10944  ltexprlem2  11077  ltexprlem6  11081  reclem2pr  11088  reclem3pr  11089  reclem4pr  11090  suplem1pr  11092  mulgt0sr  11145  supsrlem  11151  axrrecex  11203  axpre-sup  11209  ltlen  11362  addid0  11682  negn0  11692  negf1o  11693  mulge0b  12138  supaddc  12235  supadd  12236  supmul1  12237  supmullem1  12238  supmullem2  12239  supmul  12240  cju  12262  nnsub  12310  0mnnnnn0  12558  un0addcl  12559  un0mulcl  12560  nn0sub  12576  nn0n0n1ge2b  12595  zle0orge1  12630  peano5uzi  12707  eluzuzle  12887  zsupss  12979  elpq  13017  qbtwnre  13241  xrsupexmnf  13347  xrinfmexpnf  13348  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  supxrun  13358  ixxdisj  13402  icodisj  13516  difreicc  13524  uzsubsubfz  13586  fzadd2  13599  elfzmlbp  13679  fzofzim  13749  elfznelfzo  13811  injresinj  13827  subfzo0  13828  flval3  13855  modirr  13983  modsumfzodifsn  13985  addmodlteq  13987  ssnn0fi  14026  seqf1o  14084  expcl2lem  14114  expnegz  14137  expaddz  14147  expmulz  14149  facwordi  14328  faclbnd4lem4  14335  bccl  14361  hashnfinnn0  14400  hashgt12el  14461  hashgt12el2  14462  hashfun  14476  hashbclem  14491  hashbc  14492  hashfacen  14493  hashf1lem1  14494  hashf1  14496  hash2pwpr  14515  fundmge2nop0  14541  fi1uzind  14546  brfi1indALT  14549  swrdnd0  14695  wrdind  14760  wrd2ind  14761  swrdccatin1  14763  swrdccatin2  14767  pfxccat3  14772  pfxccat3a  14776  swrdccat3blem  14777  reuccatpfxs1  14785  cshw1  14860  cshwcsh2id  14867  wwlktovfo  14997  s3iunsndisj  15007  rtrclreclem3  15099  dfrtrcl2  15101  01sqrexlem1  15281  01sqrexlem6  15286  rexanre  15385  cau3lem  15393  2clim  15608  summo  15753  fsum2dlem  15806  fsumiun  15857  prodmo  15972  fprod2dlem  16016  bpolycl  16088  rpnnen2lem12  16261  odd2np1lem  16377  oddge22np1  16386  sqoddm1div8z  16391  sumeven  16424  pwp1fsum  16428  bitsfzo  16472  sadcaddlem  16494  gcd0id  16556  nn0expgcd  16601  algcvgblem  16614  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2  16677  coprmproddvdslem  16699  divgcdcoprm0  16702  isprm7  16745  prmdvdsexpr  16754  prmfac1  16757  qnumdencl  16776  hashdvds  16812  prm23lt5  16852  pcneg  16912  prmpwdvds  16942  prmreclem2  16955  4sqlem12  16994  vdwlem6  17024  vdwlem10  17028  vdwlem13  17031  0ram  17058  ram0  17060  ramz  17063  ramcl  17067  prmgaplem3  17091  prmgaplem4  17092  prmgaplem5  17093  prmgaplem6  17094  cshwshashlem1  17133  prmlem0  17143  firest  17477  imasaddfnlem  17573  imasvscafn  17582  mremre  17647  cicsym  17848  initoid  18046  termoid  18047  iszeroi  18054  drsdirfi  18351  odupos  18373  pospo  18390  joinfval  18418  meetfval  18432  lubun  18560  acsfiindd  18598  psss  18625  mgmpropd  18664  mndpsuppss  18778  xpsmnd0  18791  mnd1id  18793  0subm  18830  insubm  18831  sursubmefmnd  18909  injsubmefmnd  18910  smndex1mgm  18920  pwmnd  18950  dfgrp2e  18981  dfgrp3lem  19056  symgfix2  19434  f1omvdco2  19466  symggen  19488  odcau  19622  pgpfi  19623  sylow2blem3  19640  sylow3lem2  19646  lsmmod  19693  efgsfo  19757  frgpuptinv  19789  frgpnabllem1  19891  cyggeninv  19901  lt6abl  19913  cyggex2  19915  gsumval3lem2  19924  gsumval3  19925  gsum2d2  19992  dmdprdd  20019  dprd2da  20062  pgpfac1lem5  20099  pgpfac  20104  srgbinomlem4  20226  ringrng  20282  xpsring1d  20330  dvdsrtr  20368  dvdsrmul1  20369  c0snmgmhm  20462  0ring  20526  01eq0ringOLD  20531  0ring01eqbi  20532  domnmuln0  20709  abvn0b  20837  lss1d  20961  lspsolvlem  21144  lspsnat  21147  lbsextlem2  21161  lbsextlem3  21162  rnglidlmcl  21226  rngqiprngimf1  21310  xrsdsreclblem  21430  qsssubdrg  21444  prmirredlem  21483  pzriprnglem4  21495  cygznlem3  21588  obslbs  21750  dsmmacl  21761  lindfrn  21841  lmiclbs  21857  lmisfree  21862  mvrf1  22006  mplcoe5lem  22057  opsrtoslem2  22080  cply1mul  22300  coe1fzgsumdlem  22307  gsummoncoe1  22312  pf1ind  22359  evl1gsumdlem  22360  matecl  22431  mat1dimelbas  22477  scmateALT  22518  mdetdiaglem  22604  mdet0  22612  mdetunilem9  22626  gsummatr01  22665  cpmatmcllem  22724  m2cpminvid2lem  22760  pmatcollpw3fi1lem2  22793  chfacfscmul0  22864  chfacfpmmul0  22868  cayhamlem3  22893  tgcl  22976  tgidm  22987  indistopon  23008  fctop  23011  cctop  23013  ppttop  23014  pptbas  23015  epttop  23016  opnnei  23128  neiptopnei  23140  tgrest  23167  restntr  23190  perfopn  23193  ordtrest2lem  23211  isreg2  23385  lmmo  23388  ordthauslem  23391  cmpsublem  23407  cmpsub  23408  cmpcld  23410  hauscmplem  23414  iunconnlem  23435  unconn  23437  2ndcrest  23462  2ndcctbss  23463  2ndcdisj  23464  dis2ndc  23468  locfincmp  23534  comppfsc  23540  txbas  23575  ptbasin  23585  ptbasfi  23589  txcls  23612  txbasval  23614  ptpjopn  23620  ptclsg  23623  dfac14lem  23625  xkoccn  23627  txcnp  23628  txindis  23642  txdis1cn  23643  tx1stc  23658  tx2ndc  23659  txkgen  23660  xkoco1cn  23665  xkoco2cn  23666  xkococn  23668  xkoinjcn  23695  txconn  23697  fbfinnfr  23849  opnfbas  23850  filtop  23863  isfild  23866  fbunfip  23877  filconn  23891  fbasrn  23892  filuni  23893  isufil2  23916  filssufilg  23919  ufileu  23927  filufint  23928  rnelfmlem  23960  rnelfm  23961  fmfnfmlem2  23963  fmfnfmlem4  23965  fmfnfm  23966  hausflimi  23988  hauspwpwf1  23995  flffbas  24003  flftg  24004  alexsublem  24052  alexsubALTlem1  24055  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  ptcmplem3  24062  cldsubg  24119  qustgpopn  24128  tgptsmscld  24159  tsmsxplem1  24161  ustfilxp  24221  imasdsf1olem  24383  bldisj  24408  xbln0  24424  prdsxmslem2  24542  xrsblre  24833  icccmplem2  24845  reconn  24850  opnreen  24853  xrge0tsms  24856  metdsre  24875  iccpnfcnv  24975  cnheiborlem  24986  phtpc01  25028  pi1blem  25072  tcphcph  25271  cfilfcls  25308  iscau4  25313  bcthlem5  25362  bcth3  25365  cmssmscld  25384  hlhil  25477  ovolctb  25525  ovoliunlem2  25538  ovoliunnul  25542  ovolicc2  25557  volfiniun  25582  iundisj  25583  dyadmax  25633  dyadmbllem  25634  vitalilem2  25644  ismbfd  25674  mbfimaopnlem  25690  itg11  25726  i1faddlem  25728  mbfi1fseqlem4  25753  bddmulibl  25874  limciun  25929  perfdvf  25938  rolle  26028  dvivthlem1  26047  dvne0  26050  lhop1  26053  lhop2  26054  itgsubst  26090  dvdsq1p  26202  fta1g  26209  dgrco  26315  plydivex  26339  fta1  26350  ulmcaulem  26437  abelthlem2  26476  pilem2  26496  cxpmul2z  26733  cxpcn3lem  26790  xrlimcnp  27011  jensen  27032  wilthlem2  27112  wilthlem3  27113  muval2  27177  sqf11  27182  ppiublem1  27246  fsumvma  27257  lgsdir2lem2  27370  lgsdir2lem5  27373  lgsqrmodndvds  27397  gausslemma2dlem1a  27409  gausslemma2dlem3  27412  gausslemma2d  27418  2lgsoddprmlem2  27453  2sqreultlem  27491  2sqreunnltlem  27494  2sqreulem3  27497  dchrisum0fno1  27555  pntlem3  27653  pntleml  27655  ostthlem1  27671  ostth2lem2  27678  nosepon  27710  noextendseq  27712  nolesgn2ores  27717  nogesgn1ores  27719  nosepdmlem  27728  nodenselem8  27736  noinfno  27763  noetasuplem4  27781  nocvxmin  27823  scutun12  27855  madebdayim  27926  sltlpss  27945  addsproplem2  28003  sleadd1  28022  addsuniflem  28034  negsproplem2  28061  negsid  28073  negsunif  28087  mulsproplem9  28150  ssltmul1  28173  ssltmul2  28174  precsexlem10  28240  precsexlem11  28241  sltonold  28283  elnns2  28344  n0subs  28360  dfnns2  28362  peano5uzs  28390  recut  28428  0reno  28429  colinearalg  28925  axcontlem2  28980  axcontlem8  28986  edgupgr  29151  umgrpredgv  29157  numedglnl  29161  ausgrumgri  29184  ausgrusgri  29185  ushgredgedg  29246  ushgredgedgloop  29248  uhgr0v0e  29255  subumgredg2  29302  uhgrspansubgrlem  29307  uhgrspan1  29320  upgrreslem  29321  umgrreslem  29322  upgrres1  29330  fusgrfisstep  29346  nbuhgr  29360  nbuhgr2vtx1edgblem  29368  nbuhgr2vtx1edgb  29369  uhgrnbgr0nb  29371  edgnbusgreu  29384  nbusgredgeu0  29385  nbusgrf1o0  29386  nbusgrvtxm1uvtx  29422  cusgredg  29441  cusgrfi  29476  usgredgsscusgredg  29477  1loopgrnb0  29520  usgrvd0nedg  29551  uhgrvd00  29552  upgriswlk  29659  upgrwlkcompim  29661  uspgr2wlkeq  29664  uspgr2wlkeqi  29666  wlkv0  29669  wlkp1lem6  29696  lfgrwlkprop  29705  2pthnloop  29751  spthdep  29754  upgrwlkdvdelem  29756  usgr2wlkneq  29776  usgr2trlncl  29780  pthdlem1  29786  pthdlem2lem  29787  clwlkl1loop  29803  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  crctcshwlkn0  29841  0enwwlksnge1  29884  wlkiswwlks2  29895  wlkiswwlksupgr2  29897  wspthsnonn0vne  29937  umgr2adedgspth  29968  clwlkclwwlklem2a4  30016  clwlkclwwlklem2  30019  clwlkclwwlkf  30027  clwlkclwwlkfo  30028  erclwwlktr  30041  clwwlkf1  30068  erclwwlkntr  30090  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwwlknonex2e  30129  eucrctshift  30262  3cyclfrgrrn1  30304  frgrnbnb  30312  frgrncvvdeqlem2  30319  frgrncvvdeqlem3  30320  frgrncvvdeqlem9  30326  frgrwopreglem4a  30329  frgrwopregbsn  30336  frgrwopreg1  30337  frgrwopreg2  30338  frgrwopreglem5lem  30339  frgrwopreglem5ALT  30341  frgr2wwlk1  30348  numclwwlk1lem2foa  30373  numclwwlk1lem2f1  30376  wlkl0  30386  lnon0  30817  shmodsi  31408  shlub  31433  spanunsni  31598  h1datomi  31600  stm1ri  32263  stadd3i  32267  mdsl1i  32340  cvmdi  32343  superpos  32373  chjatom  32376  chirredi  32413  atcvat4i  32416  sumdmdii  32434  sumdmdlem  32437  cdj3lem2a  32455  cdj3lem3a  32458  cdj3i  32460  iunrnmptss  32578  disji2f  32590  disjif2  32594  iundisjf  32602  rnmposs  32684  iundisjfi  32798  nn0min  32822  wrdt2ind  32938  xrge0tsmsd  33065  cnre2csqima  33910  ordtrest2NEWlem  33921  xrge0iifcnv  33932  lmxrge0  33951  measdivcstALTV  34226  dya2iocuni  34285  omssubadd  34302  eulerpartlems  34362  bnj849  34939  bnj1118  34998  loop1cycl  35142  cusgracyclt3v  35161  derangenlem  35176  erdszelem9  35204  pconnconn  35236  iccllysconn  35255  cvmsval  35271  cvmscld  35278  cvmsss2  35279  cvmopnlem  35283  cvmfolem  35284  cvmliftmolem2  35287  cvmlift2lem10  35317  cvmlift2lem12  35319  cvmlift3lem5  35328  cvmlift3lem8  35331  satfdmlem  35373  satfrnmapom  35375  fmla1  35392  goalr  35402  fmlasucdisj  35404  satffunlem  35406  satffunlem1lem1  35407  satffunlem2lem1  35409  satffunlem2lem2  35411  msubvrs  35565  mthmblem  35585  untsucf  35710  nepss  35718  dfon2lem5  35788  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  rdgprc  35795  wzel  35825  wsuclem  35826  funpartfun  35944  altopth1  35966  altopth2  35967  colineardim1  36062  lineext  36077  btwnconn1lem14  36101  brsegle  36109  hilbert1.2  36156  trer  36317  elicc3  36318  finminlem  36319  fneint  36349  fnessref  36358  refssfne  36359  neibastop1  36360  neibastop2lem  36361  neibastop2  36362  fnemeet2  36368  fnejoin2  36370  tailfb  36378  arg-ax  36417  ordtoplem  36436  onsuct0  36442  bj-gl4  36596  bj-nfimt  36639  bj-nnfim  36747  bj-nnfor  36751  bj-nnford  36752  bj-nnflemee  36764  bj-19.36im  36772  bj-19.37im  36773  bj-sngltag  36984  bj-restn0  37091  bj-0int  37102  bj-ismooredr2  37111  bj-bary1lem1  37312  icorempo  37352  icoreresf  37353  relowlssretop  37364  rdgssun  37379  exrecfnlem  37380  finxpreclem6  37397  pibt2  37418  fin2so  37614  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  mblfinlem1  37664  mblfinlem4  37667  ovoliunnfl  37669  itg2addnclem  37678  itg2addnclem2  37679  areacirc  37720  unirep  37721  filbcmb  37747  sdclem1  37750  fdc  37752  nninfnub  37758  isbnd2  37790  ssbnd  37795  prdsbnd2  37802  cntotbnd  37803  heibor1lem  37816  heiborlem1  37818  heiborlem4  37821  heiborlem6  37823  0idl  38032  intidl  38036  unichnidl  38038  keridl  38039  prnc  38074  iss2  38345  mopickr  38364  refressn  38444  eqvreldisj  38615  erimeq  38680  disjlem17  38800  eldisjlem19  38811  prtlem17  38877  prter2  38882  ax12indn  38944  lsatn0  39000  lsatcmp  39004  lssat  39017  lfl1  39071  lshpsmreu  39110  lkrin  39165  glbconxN  39380  cvrat4  39445  paddasslem17  39838  pmodlem2  39849  dalawlem14  39886  pclclN  39893  pclfinN  39902  pclfinclN  39952  poml4N  39955  osumcllem8N  39965  pexmidlem5N  39976  cdleme32a  40443  cdlemg33b0  40703  tendoeq2  40776  diaelrnN  41047  dihmeetlem1N  41292  dihglblem5apreN  41293  dihglblem2N  41296  dochvalr  41359  dochkrshp  41388  lcfl6  41502  lcfrvalsnN  41543  mapdordlem2  41639  mapdh8b  41782  mapdh9a  41791  hdmap14lem13  41882  indstrd  42194  supinf  42283  fsuppind  42600  nna4b4nsq  42670  3cubes  42701  eldioph2b  42774  eldiophss  42785  diophren  42824  ctbnfien  42829  rencldnfilem  42831  pellexlem3  42842  pellexlem5  42844  pellex  42846  pell14qrexpcl  42878  pellfundre  42892  pellfundge  42893  pellfundlb  42895  pellfundglb  42896  jm2.19lem4  43004  fnwe2lem2  43063  pwssplit4  43101  hbtlem5  43140  cantnfresb  43337  naddwordnexlem4  43414  safesnsupfiss  43428  ss2iundf  43672  relexpmulg  43723  relexpxpmin  43730  relexpaddss  43731  dftrcl3  43733  dfrtrcl3  43746  clsk1indlem3  44056  isotone1  44061  isotone2  44062  ntrneiel2  44099  ntrneik4w  44113  rexlimdvaacbv  44218  rexlimddvcbvw  44219  ismnushort  44320  onfrALT  44569  ax6e2ndeq  44579  snssiALT  44848  relpmin  44973  relpfrlem  44974  trfr  44979  traxext  44994  modelaxreplem1  44995  iinssf  45143  hirstL-ax3  46904  fsetsnfo  47065  cfsetsnfsetf1  47071  cfsetsnfsetfo  47072  fcoresf1  47081  euoreqb  47121  2reu8i  47125  otiunsndisjX  47291  f1oresf1o2  47303  subsubelfzo0  47338  m1modnep2mod  47354  iccpartiltu  47409  iccpartigtl  47410  iccpartltu  47412  ichnfim  47451  ichnreuop  47459  ichreuopeq  47460  sprsymrelf1lem  47478  sprsymrelfolem2  47480  sprsymrelf1  47483  sprsymrelfo  47484  prproropf1olem2  47491  prproropf1olem4  47493  paireqne  47498  reuopreuprim  47513  fmtnofac2lem  47555  fmtno4prmfac  47559  prmdvdsfmtnof1lem1  47571  lighneallem2  47593  opoeALTV  47670  opeoALTV  47671  even3prm2  47706  fpprel2  47728  gbegt5  47748  gbowgt5  47749  sbgoldbwt  47764  sbgoldbst  47765  sbgoldbalt  47768  sbgoldbm  47771  mogoldbb  47772  sbgoldbo  47774  nnsum3primesle9  47781  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem1  47792  bgoldbtbndlem4  47795  bgoldbtbnd  47796  elclnbgrelnbgr  47812  grimuhgr  47878  gricushgr  47886  gricsym  47890  cycl3grtrilem  47913  isubgr3stgrlem4  47936  uspgrlimlem2  47956  uspgrlimlem3  47957  uspgrlim  47959  ceilhalfelfzo1  48016  upgrwlkupwlk  48056  copisnmnd  48085  mgm2mgm  48143  ztprmneprm  48263  lindslinindimp2lem4  48378  lindslinindsimp2  48380  lindsrng01  48385  snlindsntor  48388  ldepspr  48390  isldepslvec2  48402  suppdm  48427  blen1b  48509  dignn0ldlem  48523  digexp  48528  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  prelrrx2b  48635  eenglngeehlnmlem1  48658  line2ylem  48672  line2xlem  48674  itschlc0xyqsol1  48687  itschlc0xyqsol  48688  itsclc0  48692  2itscp  48702  inlinecirc02plem  48707  opnneilv  48806  oppcmndclem  48905  iunord  49195  tfis2d  49199