Theorem syl5bi 243

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 217	. 2 ⊢ (𝜑 → 𝜓)
3		syl5bi.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  3imtr4g  297  3orel1  1082  axc16nf  2225  ax13  2345  2euexv  2684  2euex  2694  2eu1OLD  2704  eqneqall  2993  necon3bd  2996  pm2.61dne  3069  elnelall  3101  spcimgft  3524  rspc  3548  rspcimdv  3555  rspc2gv  3566  euind  3644  reuind  3673  2reurex  3679  sbciegft  3732  rspsbc  3785  elneeldif  3868  ssexnelpss  4006  ralnralall  4366  pwpw0  4647  sssn  4660  prnebg  4687  pwsnALT  4732  intss1  4791  intmin  4796  uniintsn  4813  iinss  4873  iinss2  4874  disji2  4940  disjiun  4944  disjiund  4947  disjxiun  4953  trel3  5065  trin  5067  eusvnfb  5178  reusv3  5190  axprlem2  5209  copsexg  5266  propeqop  5281  otiunsndisj  5294  iunopeqop  5295  po3nr  5368  fri  5397  wefrc  5429  wereu2  5432  ssrelrel  5547  relop  5599  iss  5776  poirr2  5852  xpcan  5901  xpcan2  5902  sossfld  5911  wfi  6048  wfis2fg  6052  onfr  6097  onmindif  6147  funopg  6251  funssres  6260  funun  6262  fv3  6548  fvmptt  6645  iinpreima  6693  fvn0ssdmfun  6698  dff3  6720  dff4  6721  fmptsng  6784  fmptsnd  6785  tpres  6821  fnprb  6828  fntpb  6829  fvclss  6857  fpropnf1  6881  isomin  6944  isofrlem  6947  weniso  6961  oprabid  7038  ssorduni  7347  onmindif2  7374  limuni3  7414  tfis2f  7417  tfinds  7421  tfinds2  7425  tfinds3  7426  funcnvuni  7483  f1oweALT  7520  funeldmdif  7594  f1o2ndf1  7662  poxp  7666  soxp  7667  fnse  7671  suppimacnv  7683  mpoxopynvov0g  7722  reldmtpos  7742  rntpos  7747  wfrlem14  7811  wfrlem15  7812  onfununi  7821  smoiun  7841  tfrlem1  7855  tfr3  7878  frsucmptn  7917  tz7.49  7923  oaordi  8013  oawordeulem  8021  omeulem1  8049  oeordi  8054  oelimcl  8067  nnaordi  8085  nneob  8120  omsmolem  8121  erdisj  8182  qsss  8199  uniinqs  8218  map0g  8288  resixpfo  8338  ixpsnf1o  8340  xpdom3  8452  mapdom3  8526  phplem4  8536  php3  8540  unxpdomlem3  8560  ssfi  8574  findcard2  8594  findcard3  8597  frfi  8599  isfiniteg  8614  xpfi  8625  fiint  8631  finsschain  8667  dffi2  8723  marypha1lem  8733  marypha2  8739  supmo  8752  suplub2  8761  infmo  8795  ordiso2  8815  ordtypelem7  8824  ordtypelem8  8825  brwdom2  8873  unxpwdom2  8888  ixpiunwdom  8891  elirrv  8896  suc11reg  8917  noinfep  8958  cantnfle  8969  cantnflem1  8987  cantnf  8991  trcl  9005  epfrs  9008  rankpwi  9087  rankunb  9114  rankuni2b  9117  rankxplim3  9145  cplem1  9153  karden  9159  carddom2  9241  fseqenlem2  9286  ac10ct  9295  acni2  9307  acndom  9312  infpwfien  9323  alephordi  9335  alephord  9336  iunfictbso  9375  aceq3lem  9381  dfac5  9389  dfac2b  9391  dfac12lem3  9406  dfac12r  9407  cdainflem  9448  cfub  9506  cfeq0  9513  coflim  9518  cfslb2n  9525  cofsmo  9526  coftr  9530  infpssr  9565  fin23lem7  9573  fin23lem11  9574  fin23lem21  9596  isf32lem2  9611  isf34lem4  9634  isfin1-2  9642  isfin1-3  9643  fin1a2lem9  9665  fin1a2lem11  9667  fin1a2lem12  9668  fin1a2lem13  9669  domtriomlem  9699  axdc3lem2  9708  axcclem  9714  ac6c4  9738  zorn2lem4  9756  zorn2lem5  9757  zorn2lem7  9759  ttukeylem5  9770  ttukeyg  9774  brdom6disj  9789  fnrndomg  9793  iunfo  9796  iundom2g  9797  ficard  9822  konigthlem  9825  alephval2  9829  pwcfsdom  9840  fpwwe2lem9  9895  fpwwe2lem11  9897  fpwwe2lem12  9898  fpwwe2lem13  9899  pwfseqlem3  9917  gchpwdom  9927  winalim2  9953  gchina  9956  wunex2  9995  tskr1om2  10025  tskxpss  10029  inar1  10032  tskuni  10040  gruun  10063  grudomon  10074  grur1  10077  ltmpi  10161  ltexprlem2  10294  ltexprlem6  10298  reclem2pr  10305  reclem3pr  10306  reclem4pr  10307  suplem1pr  10309  mulgt0sr  10362  supsrlem  10368  axrrecex  10420  axpre-sup  10426  ltlen  10577  addid0  10896  negn0  10906  negf1o  10907  mulge0b  11347  supaddc  11445  supadd  11446  supmul1  11447  supmullem1  11448  supmullem2  11449  supmul  11450  cju  11471  nnsub  11518  0mnnnnn0  11766  un0addcl  11767  un0mulcl  11768  nn0sub  11784  nn0n0n1ge2b  11800  zle0orge1  11835  peano5uzi  11909  eluzuzle  12091  zsupss  12175  elpq  12213  qbtwnre  12431  xrsupexmnf  12537  xrinfmexpnf  12538  xrsupsslem  12539  xrinfmsslem  12540  xrub  12544  supxrun  12548  ixxdisj  12592  icodisj  12701  difreicc  12709  uzsubsubfz  12768  fzadd2  12781  elfzmlbp  12857  fzofzim  12922  elfznelfzo  12980  injresinj  12996  subfzo0  12997  flval3  13023  modirr  13148  modsumfzodifsn  13150  addmodlteq  13152  ssnn0fi  13191  seqf1o  13249  expcl2lem  13279  expnegz  13301  expaddz  13311  expmulz  13313  facwordi  13487  faclbnd4lem4  13494  bccl  13520  hashnfinnn0  13560  hashgt12el  13619  hashgt12el2  13620  hashfun  13634  hashbclem  13646  hashbc  13647  hashfacen  13648  hashf1lem1  13649  hashf1  13651  hash2pwpr  13668  fundmge2nop0  13684  fi1uzind  13689  brfi1indALT  13692  swrdnd0  13843  wrdind  13908  wrd2ind  13909  swrdccatin1  13911  swrdccatin2  13915  pfxccat3  13920  pfxccat3a  13924  swrdccat3blem  13925  reuccatpfxs1  13933  cshw1  14008  cshwcsh2id  14014  wwlktovfo  14144  s3iunsndisj  14150  rtrclreclem3  14241  dfrtrcl2  14243  sqrlem1  14424  sqrlem6  14429  rexanre  14528  cau3lem  14536  2clim  14751  summo  14895  fsum2dlem  14946  fsumiun  14997  prodmo  15111  fprod2dlem  15155  bpolycl  15227  rpnnen2lem12  15399  odd2np1lem  15510  oddge22np1  15519  sqoddm1div8z  15524  sumeven  15559  pwp1fsum  15563  bitsfzo  15605  sadcaddlem  15627  gcd0id  15688  algcvgblem  15738  lcmfunsnlem1  15798  lcmfunsnlem2lem1  15799  lcmfunsnlem2  15801  coprmproddvdslem  15823  divgcdcoprm0  15826  isprm7  15869  prmdvdsexpr  15878  prmfac1  15880  qnumdencl  15896  hashdvds  15929  prm23lt5  15968  pcneg  16027  prmpwdvds  16057  prmreclem2  16070  4sqlem12  16109  vdwlem6  16139  vdwlem10  16143  vdwlem13  16146  0ram  16173  ram0  16175  ramz  16178  ramcl  16182  prmgaplem3  16206  prmgaplem4  16207  prmgaplem5  16208  prmgaplem6  16209  cshwshashlem1  16246  prmlem0  16256  firest  16523  imasaddfnlem  16618  imasvscafn  16627  mremre  16692  cicsym  16891  initoid  17082  termoid  17083  iszeroi  17086  drsdirfi  17365  pospo  17400  joinfval  17428  meetfval  17442  lubun  17550  odupos  17562  acsfiindd  17604  psss  17641  mnd1id  17759  dfgrp2e  17875  dfgrp3lem  17942  symgfix2  18263  f1omvdco2  18295  symggen  18317  odcau  18447  pgpfi  18448  sylow2blem3  18465  sylow3lem2  18471  lsmmod  18516  efgsfo  18580  frgpuptinv  18612  frgpnabllem1  18704  cyggeninv  18713  lt6abl  18724  cyggex2  18726  gsumval3lem2  18735  gsumval3  18736  gsum2d2  18802  dmdprdd  18826  dprd2da  18869  pgpfac1lem5  18906  pgpfac  18911  srgbinomlem4  18971  dvdsrtr  19080  dvdsrmul1  19081  lss1d  19413  lspsolvlem  19592  lspsnat  19595  lbsextlem2  19609  lbsextlem3  19610  0ring  19720  01eq0ring  19722  0ring01eqbi  19723  rng1nfld  19728  domnmuln0  19748  abvn0b  19752  mvrf1  19881  mplcoe5lem  19923  opsrtoslem2  19940  cply1mul  20133  coe1fzgsumdlem  20140  gsummoncoe1  20143  pf1ind  20188  evl1gsumdlem  20189  xrsdsreclblem  20261  qsssubdrg  20274  prmirredlem  20310  cygznlem3  20386  obslbs  20544  dsmmacl  20555  lindfrn  20635  lmiclbs  20651  lmisfree  20656  matecl  20706  mat1dimelbas  20752  scmateALT  20793  mdetdiaglem  20879  mdet0  20887  mdetunilem9  20901  gsummatr01  20940  cpmatmcllem  20998  m2cpminvid2lem  21034  pmatcollpw3fi1lem2  21067  chfacfscmul0  21138  chfacfpmmul0  21142  cayhamlem3  21167  tgcl  21249  tgidm  21260  indistopon  21281  fctop  21284  cctop  21286  ppttop  21287  pptbas  21288  epttop  21289  opnnei  21400  neiptopnei  21412  tgrest  21439  restntr  21462  perfopn  21465  ordtrest2lem  21483  isreg2  21657  lmmo  21660  ordthauslem  21663  cmpsublem  21679  cmpsub  21680  cmpcld  21682  hauscmplem  21686  iunconnlem  21707  unconn  21709  2ndcrest  21734  2ndcctbss  21735  2ndcdisj  21736  dis2ndc  21740  locfincmp  21806  comppfsc  21812  txbas  21847  ptbasin  21857  ptbasfi  21861  txcls  21884  txbasval  21886  ptpjopn  21892  ptclsg  21895  dfac14lem  21897  xkoccn  21899  txcnp  21900  txindis  21914  txdis1cn  21915  tx1stc  21930  tx2ndc  21931  txkgen  21932  xkoco1cn  21937  xkoco2cn  21938  xkococn  21940  xkoinjcn  21967  txconn  21969  fbfinnfr  22121  opnfbas  22122  filtop  22135  isfild  22138  fbunfip  22149  filconn  22163  fbasrn  22164  filuni  22165  isufil2  22188  filssufilg  22191  ufileu  22199  filufint  22200  rnelfmlem  22232  rnelfm  22233  fmfnfmlem2  22235  fmfnfmlem4  22237  fmfnfm  22238  hausflimi  22260  hauspwpwf1  22267  flffbas  22275  flftg  22276  alexsublem  22324  alexsubALTlem1  22327  alexsubALTlem2  22328  alexsubALTlem3  22329  alexsubALTlem4  22330  alexsubALT  22331  ptcmplem3  22334  cldsubg  22390  qustgpopn  22399  tgptsmscld  22430  tsmsxplem1  22432  ustfilxp  22492  imasdsf1olem  22654  bldisj  22679  xbln0  22695  prdsxmslem2  22810  xrsblre  23090  icccmplem2  23102  reconn  23107  opnreen  23110  xrge0tsms  23113  metdsre  23132  iccpnfcnv  23219  cnheiborlem  23229  phtpc01  23271  pi1blem  23314  tcphcph  23511  cfilfcls  23548  iscau4  23553  bcthlem5  23602  bcth3  23605  cmssmscld  23624  hlhil  23717  ovolctb  23762  ovoliunlem2  23775  ovoliunnul  23779  ovolicc2  23794  volfiniun  23819  iundisj  23820  dyadmax  23870  dyadmbllem  23871  vitalilem2  23881  ismbfd  23911  mbfimaopnlem  23927  itg11  23963  i1faddlem  23965  mbfi1fseqlem4  23990  bddmulibl  24110  limciun  24163  perfdvf  24172  rolle  24258  dvivthlem1  24276  dvne0  24279  lhop1  24282  lhop2  24283  itgsubst  24317  dvdsq1p  24425  fta1g  24432  dgrco  24536  plydivex  24557  fta1  24568  ulmcaulem  24653  abelthlem2  24691  pilem2  24711  cxpmul2z  24943  cxpcn3lem  24997  xrlimcnp  25216  jensen  25236  wilthlem2  25316  wilthlem3  25317  muval2  25381  sqf11  25386  ppiublem1  25448  fsumvma  25459  lgsdir2lem2  25572  lgsdir2lem5  25575  lgsqrmodndvds  25599  gausslemma2dlem1a  25611  gausslemma2dlem3  25614  gausslemma2d  25620  2lgsoddprmlem2  25655  2sqreultlem  25693  2sqreunnltlem  25696  2sqreulem3  25699  dchrisum0fno1  25757  pntlem3  25855  pntleml  25857  ostthlem1  25873  ostth2lem2  25880  colinearalg  26367  axcontlem2  26422  axcontlem8  26428  edgupgr  26590  umgrpredgv  26596  numedglnl  26600  ausgrumgri  26623  ausgrusgri  26624  ushgredgedg  26682  ushgredgedgloop  26684  uhgr0v0e  26691  subumgredg2  26738  uhgrspansubgrlem  26743  uhgrspan1  26756  upgrreslem  26757  umgrreslem  26758  upgrres1  26766  fusgrfisstep  26782  nbuhgr  26796  nbuhgr2vtx1edgblem  26804  nbuhgr2vtx1edgb  26805  uhgrnbgr0nb  26807  edgnbusgreu  26820  nbusgredgeu0  26821  nbusgrf1o0  26822  nbusgrvtxm1uvtx  26858  cusgredg  26877  cusgrfi  26911  usgredgsscusgredg  26912  1loopgrnb0  26955  usgrvd0nedg  26986  uhgrvd00  26987  upgriswlk  27093  upgrwlkcompim  27095  uspgr2wlkeq  27098  uspgr2wlkeqi  27100  wlkv0  27103  wlklenvclwlk  27107  wlkp1lem6  27133  lfgrwlkprop  27142  2pthnloop  27187  spthdep  27190  upgrwlkdvdelem  27192  usgr2wlkneq  27212  usgr2trlncl  27216  pthdlem1  27222  pthdlem2lem  27223  clwlkl1loop  27239  crctcshwlkn0lem3  27265  crctcshwlkn0lem5  27267  crctcshwlkn0  27274  0enwwlksnge1  27317  wlkiswwlks2  27328  wlkiswwlksupgr2  27330  wspthsnonn0vne  27371  umgr2adedgspth  27402  clwlkclwwlklem2a4  27450  clwlkclwwlklem2  27453  clwlkclwwlkf  27461  clwlkclwwlkfo  27462  erclwwlktr  27475  clwwlkf1  27503  erclwwlkntr  27525  hashecclwwlkn1  27531  umgrhashecclwwlk  27532  clwwlknonex2e  27564  eucrctshift  27698  3cyclfrgrrn1  27744  frgrnbnb  27752  frgrncvvdeqlem2  27759  frgrncvvdeqlem3  27760  frgrncvvdeqlem9  27766  frgrwopreglem4a  27769  frgrwopregbsn  27776  frgrwopreg1  27777  frgrwopreg2  27778  frgrwopreglem5lem  27779  frgrwopreglem5ALT  27781  frgr2wwlk1  27788  numclwwlk1lem2foa  27813  numclwwlk1lem2f1  27816  wlkl0  27826  lnon0  28254  shmodsi  28845  shlub  28870  spanunsni  29035  h1datomi  29037  stm1ri  29700  stadd3i  29704  mdsl1i  29777  cvmdi  29780  superpos  29810  chjatom  29813  chirredi  29850  atcvat4i  29853  sumdmdii  29871  sumdmdlem  29874  cdj3lem2a  29892  cdj3lem3a  29895  cdj3i  29897  iunrnmptss  29986  disji2f  29993  disjif2  29997  iundisjf  30005  rnmposs  30082  iundisjfi  30177  nn0min  30192  wrdt2ind  30277  xrge0tsmsd  30460  cnre2csqima  30727  ordtrest2NEWlem  30738  xrge0iifcnv  30749  lmxrge0  30768  measdivcstALTV  31057  dya2iocuni  31114  omssubadd  31131  eulerpartlems  31191  bnj849  31769  bnj1118  31826  loop1cycl  31948  cusgracyclt3v  31967  derangenlem  31982  erdszelem9  32010  pconnconn  32042  iccllysconn  32061  cvmsval  32077  cvmscld  32084  cvmsss2  32085  cvmopnlem  32089  cvmfolem  32090  cvmliftmolem2  32093  cvmlift2lem10  32123  cvmlift2lem12  32125  cvmlift3lem5  32134  cvmlift3lem8  32137  satfdmlem  32177  satfrnmapom  32179  fmla1  32196  goalr  32205  fmlasucdisj  32207  satffunlem  32209  satffunlem1lem1  32210  satffunlem2lem1  32212  satffunlem2lem2  32214  msubvrs  32360  mthmblem  32380  untsucf  32489  3orel2  32494  3orel3  32495  nepss  32501  eqfunresadj  32557  dfon2lem5  32585  dfon2lem6  32586  dfon2lem7  32587  dfon2lem8  32588  rdgprc  32593  trpredtr  32623  dftrpred3g  32626  trpredrec  32631  frpomin  32632  frpoind  32634  frpoins2fg  32636  frmin  32638  frind  32639  frins2fg  32643  wzel  32665  wsuclem  32666  fpr3g  32676  frrlem9  32685  frrlem10  32686  frrlem12  32688  frrlem13  32689  nosepon  32726  noextendseq  32728  nolesgn2ores  32733  nosepdmlem  32741  nodenselem8  32749  noetalem3  32773  nocvxmin  32802  scutun12  32825  funpartfun  32958  altopth1  32980  altopth2  32981  colineardim1  33076  lineext  33091  btwnconn1lem14  33115  brsegle  33123  hilbert1.2  33170  trer  33218  elicc3  33219  finminlem  33220  fneint  33250  fnessref  33259  refssfne  33260  neibastop1  33261  neibastop2lem  33262  neibastop2  33263  fnemeet2  33269  fnejoin2  33271  tailfb  33279  arg-ax  33317  ordtoplem  33336  onsuct0  33342  bj-gl4lem  33478  bj-nfimt  33517  bj-nnfim  33805  bj-nnfort  33808  bj-nnflemee  33820  bj-sngltag  33846  bj-restn0  33926  bj-0int  33938  bj-ismooredr2  33948  bj-bary1lem1  34075  icorempo  34109  icoreresf  34110  relowlssretop  34121  rdgssun  34136  exrecfnlem  34137  finxpreclem6  34154  pibt2  34175  fin2so  34356  poimirlem24  34393  poimirlem25  34394  poimirlem26  34395  poimirlem27  34396  poimirlem29  34398  poimirlem30  34399  poimirlem31  34400  mblfinlem1  34406  mblfinlem4  34409  ovoliunnfl  34411  itg2addnclem  34420  itg2addnclem2  34421  areacirc  34464  unirep  34466  filbcmb  34493  sdclem1  34496  fdc  34498  nninfnub  34504  isbnd2  34539  ssbnd  34544  prdsbnd2  34551  cntotbnd  34552  heibor1lem  34565  heiborlem1  34567  heiborlem4  34570  heiborlem6  34572  0idl  34781  intidl  34785  unichnidl  34787  keridl  34788  prnc  34823  iss2  35083  eqvreldisj  35330  erim  35393  prtlem17  35493  prter2  35498  ax12indn  35560  lsatn0  35616  lsatcmp  35620  lssat  35633  lfl1  35687  lshpsmreu  35726  lkrin  35781  glbconxN  35995  cvrat4  36060  paddasslem17  36453  pmodlem2  36464  dalawlem14  36501  pclclN  36508  pclfinN  36517  pclfinclN  36567  poml4N  36570  osumcllem8N  36580  pexmidlem5N  36591  cdleme32a  37058  cdlemg33b0  37318  tendoeq2  37391  diaelrnN  37662  dihmeetlem1N  37907  dihglblem5apreN  37908  dihglblem2N  37911  dochvalr  37974  dochkrshp  38003  lcfl6  38117  lcfrvalsnN  38158  mapdordlem2  38254  mapdh8b  38397  mapdh9a  38406  hdmap14lem13  38497  nn0expgcd  38656  eldioph2b  38795  eldiophss  38807  diophren  38846  ctbnfien  38851  rencldnfilem  38853  pellexlem3  38864  pellexlem5  38866  pellex  38868  pell14qrexpcl  38900  pellfundre  38914  pellfundge  38915  pellfundlb  38917  pellfundglb  38918  jm2.19lem4  39025  fnwe2lem2  39087  pwssplit4  39125  hbtlem5  39164  ss2iundf  39440  relexpmulg  39491  relexpxpmin  39498  relexpaddss  39499  dftrcl3  39501  dfrtrcl3  39514  clsk1indlem3  39829  isotone1  39834  isotone2  39835  ntrneiel2  39872  ntrneik4w  39886  rexlimdvaacbv  39998  onfrALT  40374  ax6e2ndeq  40384  snssiALT  40653  iinssf  40899  hirstL-ax3  42623  euoreqb  42778  2reu8i  42782  otiunsndisjX  42948  f1oresf1o2  42960  subsubelfzo0  42996  iccpartiltu  43018  iccpartigtl  43019  iccpartltu  43021  ichnfim  43060  ichnreuop  43070  ichreuopeq  43071  sprsymrelf1lem  43089  sprsymrelfolem2  43091  sprsymrelf1  43094  sprsymrelfo  43095  prproropf1olem2  43102  prproropf1olem4  43104  paireqne  43109  reuopreuprim  43124  fmtnofac2lem  43166  fmtno4prmfac  43170  prmdvdsfmtnof1lem1  43182  lighneallem2  43207  opoeALTV  43284  opeoALTV  43285  even3prm2  43320  fpprel2  43342  gbegt5  43362  gbowgt5  43363  sbgoldbwt  43378  sbgoldbst  43379  sbgoldbalt  43382  sbgoldbm  43385  mogoldbb  43386  sbgoldbo  43388  nnsum3primesle9  43395  nnsum4primeseven  43401  nnsum4primesevenALTV  43402  wtgoldbnnsum4prm  43403  bgoldbnnsum3prm  43405  bgoldbtbndlem1  43406  bgoldbtbndlem4  43409  bgoldbtbnd  43410  isomushgr  43427  isomuspgrlem2b  43430  isomuspgrlem2c  43431  upgrwlkupwlk  43451  mgmpropd  43478  copisnmnd  43512  mgm2mgm  43566  ringrng  43582  c0snmgmhm  43617  ztprmneprm  43827  mndpsuppss  43853  lindslinindimp2lem4  43950  lindslinindsimp2  43952  lindsrng01  43957  snlindsntor  43960  ldepspr  43962  isldepslvec2  43974  suppdm  44000  blen1b  44083  dignn0ldlem  44097  digexp  44102  nn0sumshdiglemB  44115  nn0sumshdiglem1  44116  prelrrx2b  44136  eenglngeehlnmlem1  44159  line2ylem  44173  line2xlem  44175  itschlc0xyqsol1  44188  itschlc0xyqsol  44189  itsclc0  44193  2itscp  44203  inlinecirc02plem  44208  iunord  44213  tfis2d  44217