Theorem a1i 9

Description: Inference derived from axiom ax-1 6. See a1d 22 for an explanation of our informal use of the terms "inference" and "deduction." See also the comment in syld 45. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
a1i.1	|- ph

Assertion

Ref	Expression
a1i	|- ( ps -> ph )

Proof of Theorem a1i

Step	Hyp	Ref	Expression
1		a1i.1	. 2 |- ph
2		ax-1 6	. 2 |- ( ph -> ( ps -> ph ) )
3	1, 2	ax-mp 5	1 |- ( ps -> ph )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by:  mp1i  10  imim2i  12  syl  14  mpi  15  idd  21  a1i13  24  2a1i  27  syl6  33  mpdi  43  mpii  44  mpsyl  65  syl7  69  syl8  71  syl9  72  impbid21d  127  impbid1  141  mpbii  147  mpbiri  167  biidd  171  2th  173  syl5bb  191  syl6bb  195  imbi2i  225  jca2  306  jctil  310  jctir  311  sylani  403  sylan2i  404  sylancl  409  sylancr  410  mpan  420  mpan2  421  mpani  426  mpan2i  427  anbi2i  452  anbi1i  453  nsyl3  615  mt2  629  mt2i  633  mto  651  mtoi  653  sylnib  665  simprimdc  844  con1biimdc  858  pm2.54dc  876  pm5.17dc  889  pm5.21nd  901  pm5.71dc  945  dedlema  953  dedlemb  954  a1tru  1347  xorbi12i  1361  dfbi3dc  1375  hbth  1439  dfexdc  1477  a17d  1507  nfvd  1509  nfan  1544  nfim  1551  19.21ht  1560  nfbi  1568  alrimd  1589  19.32dc  1657  equsexd  1707  spime  1719  equveli  1732  sbieh  1763  dvelimfALT2  1789  cbvald  1895  cbvexdh  1896  nfsbxy  1913  sbcomxyyz  1943  dvelimALT  1983  dvelimfv  1984  hbsb4t  1986  dvelimor  1991  eubii  2006  nfeudv  2012  nfmo  2017  mobii  2034  moimv  2063  2euswapdc  2088  eqidd  2138  syl5eq  2182  syl6eq  2186  eqeltrid  2224  eleqtrid  2226  eqeltrdi  2228  eleqtrdi  2230  nfcvd  2280  dvelimc  2300  nnedc  2311  necon1idc  2359  ralbii  2439  rexbii  2440  nfraldxy  2465  nfrexdxy  2466  nfralxy  2469  nfrexxy  2470  nfralya  2471  nfrexya  2472  rgenw  2485  ralimi  2493  rexim  2524  reximi  2527  rexlimivw  2543  r19.29af2  2570  r19.32vdc  2578  nfreudxy  2602  nfreuxy  2603  reubii  2614  rmobii  2619  rabbii  2667  ceqsralt  2708  vtoclgft  2731  rr19.28v  2819  reu8  2875  cdeqth  2891  nfsbc1d  2920  nfsbc1  2921  nfsbc  2924  sbcbii  2963  sbc2iegf  2974  sbc2iedv  2976  sbc3ie  2977  sbcrext  2981  rmob  2996  sbcnel12g  3014  sbcne12g  3015  csbcomg  3020  csbeq2i  3024  nfcsb1  3029  nfcsb  3032  csbiebt  3034  csbief  3039  csbie2t  3043  sbcnestgf  3046  sstrid  3103  sstrdi  3104  ssidd  3113  sseqtrrid  3143  eqsstrdi  3144  difssd  3198  ssconb  3204  abvor0dc  3381  rabnc  3390  nfif  3495  disjpr2  3582  tpid3g  3633  neldifsnd  3649  diftpsn3  3656  preq12bg  3695  intmin  3786  int0el  3796  dfiun2  3842  dfiin2  3843  dfiunv2  3844  iunrab  3855  iunid  3863  iun0  3864  iinrabm  3870  iunin1  3872  2iunin  3874  iinin1m  3877  breqtrid  3960  ssbri  3967  nfbr  3969  opabbii  3990  mpteq2i  4010  mpteq12i  4011  opth1  4153  copsexg  4161  copsex4g  4164  epelg  4207  issod  4236  fr0  4268  frind  4269  trsucss  4340  bm2.5ii  4407  ordsucss  4415  onsucelsucr  4419  ordunisuc2r  4425  ordirr  4452  ordfr  4484  peano5  4507  finds1  4511  ordom  4515  0elnn  4527  omsinds  4530  0nelrel  4580  csbcnvg  4718  dfiun3  4793  dfiin3  4794  dmcosseq  4805  resiun1  4833  resiun2  4834  resima2  4848  iss  4860  resiima  4892  relbrcnvg  4913  inimasn  4951  elxp4  5021  elxp5  5022  dfco2  5033  coiun  5043  relssdmrn  5054  unielrel  5061  relfld  5062  cnviinm  5075  cnvsom  5077  nfiotadw  5086  nfiotaw  5087  iota2df  5107  funssres  5160  fntp  5175  imadif  5198  imain  5200  sbcfng  5265  sbcfg  5266  fun  5290  fun11iun  5381  funcocnv2  5385  f1oprg  5404  sefvex  5435  tz6.12f  5443  dfimafn2  5464  fnsnfv  5473  ssimaex  5475  fvun1  5480  fvmptg  5490  fvmpt3i  5494  fvopab6  5510  fndmdifcom  5519  respreima  5541  fmptco  5579  fcoconst  5584  dfmpt  5590  fmptapd  5604  fmptpr  5605  isocnv2  5706  riotaexg  5727  nfriotadxy  5731  nfriota  5732  riota2f  5744  nfov  5794  oprabbii  5819  mpoeq123i  5827  ovmpt4g  5886  ovmpodxf  5889  ovmpox  5892  ovmpoga  5893  ovi3  5900  ov6g  5901  ovelrn  5912  caovcom  5921  caovass  5924  caovdi  5943  caovimo  5957  ofc12  5995  oprabex3  6020  reldm  6077  fnmpoovd  6105  oprabco  6107  oprab2co  6108  disjsnxp  6127  mpoxopoveq  6130  brtpos2  6141  reldmtpos  6143  dmtpos  6146  dftpos4  6153  tposfn2  6156  smores  6182  tfrlemisucfn  6214  tfrlemiubacc  6220  tfri1dALT  6241  tfrcl  6254  tfri1  6255  rdgon  6276  frec0g  6287  frectfr  6290  freccllem  6292  frecfcllem  6294  frecsuclem  6296  oacl  6349  omcl  6350  oeicl  6351  oawordi  6358  nnsucelsuc  6380  nntri1  6385  nnsseleq  6390  nnaord  6398  nnmordi  6405  nnmord  6406  nnaordex  6416  nnm00  6418  swoer  6450  eqer  6454  0er  6456  uniqs  6480  erinxp  6496  qliftf  6507  brecop  6512  ecopovtrn  6519  ecopover  6520  ecopoverg  6523  th3qlem1  6524  elpmg  6551  nfixpxy  6604  ixpintm  6612  ixpsnf1o  6623  brdomg  6635  en2i  6657  en3i  6658  dom2  6662  dom3  6663  ener  6666  ensymb  6667  entr  6671  fundmen  6693  mapsnen  6698  map1  6699  enpr2d  6704  xpsnen  6708  xpassen  6717  ssenen  6738  nneneq  6744  phplem4dom  6749  phpelm  6753  phplem4on  6754  fidceq  6756  fiunsnnn  6768  finexdc  6789  infm  6791  exmidpw  6795  unfidisj  6803  undifdc  6805  unfiin  6807  fiintim  6810  xpfi  6811  fisseneq  6813  ssfirab  6815  fnfi  6818  iunfidisj  6827  f1finf1o  6828  fidcenumlemrk  6835  fidcenumlemr  6836  elfi2  6853  ssfii  6855  supubti  6879  suplubti  6880  cnvinfex  6898  eqinfti  6900  infvalti  6902  inflbti  6904  ordiso2  6913  djuex  6921  inl11  6943  djuss  6948  1stinl  6952  2ndinl  6953  1stinr  6954  2ndinr  6955  updjudhcoinlf  6958  updjudhcoinrg  6959  casefun  6963  caseinl  6969  caseinr  6970  omp1eomlem  6972  endjusym  6974  difinfsn  6978  djufun  6982  ctmlemr  6986  ctm  6987  ctssdclemn0  6988  ctssdccl  6989  ctssdc  6991  finomni  7005  fodjuomnilemdc  7009  fodjuf  7010  fodjum  7011  fodju0  7012  nnnninf  7016  ctssexmid  7017  ismkvnex  7022  omnimkv  7023  mkvprop  7025  cardcl  7030  pm54.43  7039  en2other2  7045  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  acfun  7056  exmidaclem  7057  endjudisj  7059  djuen  7060  djuassen  7066  xpdjuen  7067  ccfunen  7072  elni2  7115  indpi  7143  enqeceq  7160  mulcanenqec  7187  ltnnnq  7224  enq0er  7236  enq0eceq  7238  nqnq0pi  7239  mulcanenq0ec  7246  nnnq0lem1  7247  addnq0mo  7248  mulnq0mo  7249  prarloclemlo  7295  prarloclem3  7298  genipv  7310  nqprrnd  7344  nqprdisj  7345  nqprloc  7346  1idprl  7391  1idpru  7392  recexprlemlol  7427  recexprlemupu  7429  cauappcvgprlemm  7446  cauappcvgprlemdisj  7452  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  cauappcvgpr  7463  caucvgprlemm  7469  caucvgprlemcl  7477  caucvgprlemladdrl  7479  caucvgpr  7483  caucvgprprlemml  7495  caucvgprprlemmu  7496  caucvgprprlemopu  7500  caucvgprprlemclphr  7506  suplocexprlemss  7516  suplocexprlemlub  7525  enreceq  7537  prsrlem1  7543  addsrmo  7544  mulsrmo  7545  0idsr  7568  pn0sr  7572  recexgt0sr  7574  archsr  7583  srpospr  7584  prsradd  7587  prsrlt  7588  caucvgsrlemfv  7592  caucvgsrlembound  7595  caucvgsrlemoffval  7597  caucvgsrlemoffcau  7599  caucvgsrlemoffgt1  7600  caucvgsrlemoffres  7601  caucvgsr  7603  ltpsrprg  7604  mappsrprg  7605  map2psrprg  7606  suplocsrlemb  7607  pitonnlem1p1  7647  pitoregt0  7650  recidpirqlemcalc  7658  recidpirq  7659  axcnex  7660  axmulcl  7667  axmulass  7674  axdistr  7675  ax0id  7679  axprecex  7681  axpre-ltirr  7683  axpre-lttrn  7685  axpre-ltadd  7687  axpre-mulgt0  7688  axpre-mulext  7689  axcaucvglemval  7698  axcaucvg  7701  0cnd  7752  0red  7760  1red  7774  1cnd  7775  ltxrlt  7823  1p1times  7889  nfneg  7952  negsub  8003  addlsub  8125  pncan1  8132  npcan1  8133  negf1o  8137  kcnktkm1cn  8138  mulsubfacd  8173  rereim  8341  cru  8357  apreim  8358  mulreim  8359  apadd1  8363  apneg  8366  aprcl  8401  muleqadd  8422  eqneg  8485  mulgt1  8614  suprlubex  8703  negiso  8706  dfinfre  8707  sup3exmid  8708  cju  8712  nn1suc  8732  2cnd  8786  avglt1  8951  avglt2  8952  add1p1  8962  sub1m1  8963  cnm2m1cnm3  8964  xp1d2m1eqxm1d2  8965  div4p1lem1div2  8966  nn0p1gt0  8999  un0addcl  9003  nn0ge2m1nn  9030  0zd  9059  elnn0z  9060  elznn0  9062  1zzd  9074  peano2z  9083  ztri3or0  9089  zlelttric  9092  zltnle  9093  zmulcl  9100  zltp1le  9101  zgt0ge1  9105  elz2  9115  zdceq  9119  zdclt  9121  nn0lt2  9125  nn0le2is012  9126  zneo  9145  nneo  9147  zeo2  9150  uzind  9155  uzind2  9156  nn0ind  9158  zadd2cl  9173  uzm1  9349  uzin  9351  uz3m2nn  9361  uzind4i  9380  infrenegsupex  9382  supminfex  9385  eqreznegel  9399  nn01to3  9402  nn0ge2m1nnALT  9403  divfnzn  9406  cnref1o  9433  rpnegap  9467  divlt1lt  9504  divle1le  9505  ltxr  9555  xrre3  9598  xaddf  9620  xaddval  9621  xaddnemnf  9633  xaddnepnf  9634  xaddass2  9646  xltadd1  9652  xaddge0  9654  xlt2add  9656  xleaddadd  9663  ixxssixx  9678  elioc2  9712  elico2  9713  elicc2  9714  lincmb01cmp  9779  fzdcel  9813  ige3m2fz  9822  fz01en  9826  fzdifsuc  9854  elfz1b  9863  uzsplit  9865  fseq1p1m1  9867  elfzp1b  9870  ige2m1fz1  9882  ige2m1fz  9883  0elfz  9891  fz0tp  9894  fz0fzdiffz0  9900  nn0split  9906  nnsplit  9907  fzoval  9918  fzouzsplit  9949  elfzom1elp1fzo  9972  elfzonlteqm1  9980  fzo0to3tp  9989  fzo0sn0fzo1  9991  fzosplitprm1  10004  fvinim0ffz  10011  qlelttric  10015  qltnle  10016  qdceq  10017  qbtwnrelemcalc  10026  qbtwnre  10027  ioo0  10030  ioom  10031  ico0  10032  ioc0  10033  2tnp1ge0ge0  10067  flhalf  10068  fldiv4p1lem1div2  10071  intfracq  10086  q0mod  10121  q1mod  10122  mulp1mod1  10131  modqnegd  10145  modsumfzodifsn  10162  frec2uzltd  10169  frec2uzlt2d  10170  frecfzennn  10192  uzennn  10202  1tonninf  10206  iseqvalcbv  10223  seq3val  10224  seqvalcd  10225  seq3-1  10226  seqf  10227  seq3p1  10228  seqf2  10230  seq1cd  10231  seqp1cd  10232  seq3clss  10233  monoord  10242  seq3caopr3  10247  seq3f1olemp  10268  seq3id3  10273  seq3homo  10276  seq3z  10277  ser0  10280  ser3ge0  10283  exp0  10290  expgt1  10324  ltexp2a  10338  leexp2a  10339  leexp2r  10340  exple1  10342  expubnd  10343  binom21  10397  binom2sub1  10399  zesq  10403  expnlbnd2  10410  sqeq0d  10416  sqoddm1div8  10437  expcanlem  10455  expcan  10456  nn0opthlem1d  10459  nn0opthlem2d  10460  faclbnd  10480  faclbnd2  10481  bc0k  10495  bcn1  10497  bcn2  10503  bcn2m1  10508  bcn2p1  10509  fihashen1  10538  hashunlem  10543  1elfz0hash  10545  hashprg  10547  hashdifpr  10559  hashxp  10565  zfz1isolem1  10576  seq3coll  10578  shftuz  10582  ovshftex  10584  shftfn  10589  imval  10615  crre  10622  crim  10623  remim  10625  cjreb  10631  readd  10634  remullem  10636  imadd  10642  cjadd  10649  cjreim  10668  cjreim2  10669  cjap  10671  cnrecnv  10675  cvg1nlemcxze  10747  cvg1nlemres  10750  rexfiuz  10754  r19.29uz  10757  resqrexlem1arp  10770  resqrexlemfp1  10774  resqrexlemover  10775  resqrexlemdec  10776  resqrexlemdecn  10777  resqrexlemlo  10778  resqrexlemcalc1  10779  resqrexlemcalc2  10780  resqrexlemcalc3  10781  resqrexlemnmsq  10782  resqrexlemnm  10783  resqrexlemcvg  10784  resqrexlemglsq  10787  resqrexlemga  10788  resqrexlemsqa  10789  sqrtgt0  10799  sqrtsq  10809  absimle  10849  abstri  10869  cau3lem  10879  amgm2  10883  maxabsle  10969  maxabslemab  10971  maxabslemlub  10972  maxltsup  10983  max0addsup  10984  fimaxre2  10991  minabs  11000  bdtrilem  11003  bdtri  11004  xrmaxiflemcl  11007  xrmaxiflemcom  11011  xrmaxadd  11023  infxrnegsupex  11025  xrbdtri  11038  clim  11043  climshft  11066  climle  11096  clim2ser  11099  clim2ser2  11100  iserex  11101  isermulc2  11102  climrecvg1n  11110  climcvg1nlem  11111  climcaucn  11113  sumrbdclem  11138  fsum3cvg  11139  summodclem2a  11143  sum0  11150  fisumss  11154  fsumrecl  11163  fsumzcl  11164  fsumnn0cl  11165  fsumrpcl  11166  fsumadd  11168  fsumsplitf  11170  sumsnf  11171  sumpr  11175  sumtp  11176  isumclim3  11185  isumadd  11193  sumsplitdc  11194  fsum2dlemstep  11196  fisumcom2  11200  fsumcom  11201  fisum0diag  11203  fisum0diag2  11209  fsumneg  11213  fsumconst  11216  modfsummodlemstep  11219  modfsummod  11220  fsumge0  11221  fsumlessfi  11222  fsumabs  11227  fsumrelem  11233  iserabs  11237  fsumiun  11239  hash2iun1dif1  11242  binomlem  11245  isumshft  11252  isumnn0nn  11255  isumlessdc  11258  divcnv  11259  trireciplem  11262  trirecip  11263  expcnvap0  11264  expcnvre  11265  expcnv  11266  explecnv  11267  geosergap  11268  geoserap  11269  geolim  11273  georeclim  11275  geo2sum  11276  geo2sum2  11277  geo2lim  11278  geoisumr  11280  geoisum1  11281  geoisum1c  11282  0.999...  11283  geoihalfsum  11284  cvgratnnlembern  11285  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  cvgratnnlemsumlt  11290  cvgratnnlemfm  11291  cvgratnnlemrate  11292  cvgratnn  11293  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  clim2prod  11301  clim2divap  11302  prodf1  11304  prodfrecap  11308  prodrbdclem  11333  fproddccvg  11334  efcllemp  11353  efcllem  11354  ef0lem  11355  ege2le3  11366  efcj  11368  efgt0  11379  eftlub  11385  efsep  11386  ef4p  11389  efgt1p2  11390  efgt1p  11391  sinval  11398  cosval  11399  tanval2ap  11409  tanval3ap  11410  efi4p  11413  sinadd  11432  cosadd  11433  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  sin01gt0  11457  cos12dec  11463  eirraplem  11472  nndivdvds  11488  absdvdsb  11500  dvdsabsb  11501  dvds1  11540  dvdsfac  11547  zeneo  11557  odd2np1lem  11558  even2n  11560  oexpneg  11563  oddge22np1  11567  evennn02n  11568  evennn2n  11569  2tp1odd  11570  mulsucdiv2z  11571  ltoddhalfle  11579  halfleoddlt  11580  m1expo  11586  m1exp1  11587  nn0enne  11588  nn0ehalf  11589  nn0o1gt2  11591  nno  11592  nn0o  11593  nn0oddm1d2  11595  nnoddm1d2  11596  4dvdseven  11603  flodddiv4  11620  flodddiv4lt  11622  flodddiv4t2lthalf  11623  zsupcllemex  11628  zsupcl  11629  infssuzex  11631  infssuzcldc  11633  gcddvds  11641  zeqzmulgcd  11648  gcdcom  11651  gcdabs  11665  gcdabs1  11666  dfgcd3  11687  gcdass  11692  bezoutr1  11710  nn0seqcvgd  11711  alginv  11717  algcvg  11718  algcvga  11721  algfx  11722  eucalgcvga  11728  eucalg  11729  lcmval  11733  lcmcom  11734  lcmabs  11746  lcmass  11755  ncoprmgcdne1b  11759  cncongr1  11773  prmind2  11790  dvdsnprmd  11795  prmgt1  11801  oddprmge3  11804  coprm  11811  sqrt2irrlem  11828  sqrt2irr  11829  sqrt2irr0  11831  pw2dvdslemn  11832  pw2dvdseulemle  11834  oddpwdclemxy  11836  oddpwdclemodd  11839  oddpwdclemdc  11840  oddpwdc  11841  sqpweven  11842  2sqpwodd  11843  sqrt2irraplemnn  11846  sqrt2irrap  11847  divdenle  11864  nn0gcdsq  11867  numdensq  11869  nn0sqrtelqelz  11873  dfphi2  11885  phimullem  11890  oddennn  11894  evenennn  11895  unennn  11899  ennnfonelemj0  11903  ennnfonelemg  11905  ennnfonelemh  11906  ennnfonelemp1  11908  ennnfonelem1  11909  ennnfonelemhdmp1  11911  ennnfonelemss  11912  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemex  11916  ennnfonelemhom  11917  ennnfonelemrn  11921  ennnfonelemnn0  11924  ctinfomlemom  11929  ctinf  11932  ctiunctlemuom  11938  ctiunct  11942  unct  11943  structcnvcnv  11964  strnfvn  11969  strndxid  11976  fvsetsid  11982  setsfun  11983  setsfun0  11984  setscom  11988  strslfvd  11989  strslfv2d  11990  strslfv2  11991  strslfv  11992  strslss  11995  setsslid  11998  setsslnid  11999  ressval2  12008  ressid  12009  strle1g  12038  strle2g  12039  strle3g  12040  2strbasg  12049  2stropg  12050  srngstrd  12070  lmodstrd  12081  ipsstrd  12089  istopon  12169  fiinbas  12205  baspartn  12206  eltg4i  12213  bastg  12219  unitg  12220  tgdom  12230  tgidm  12232  distop  12243  distopon  12245  epttop  12248  isopn3  12283  tgrest  12327  resttopon  12329  restin  12334  rest0  12337  lmfval  12350  cnfval  12352  cnpfval  12353  cnrest2  12394  cnrest2r  12395  cnptopresti  12396  cnptoprest  12397  cnptoprest2  12398  lmres  12406  txbasval  12425  tx1cn  12427  tx2cn  12428  txcnp  12429  txrest  12434  txdis1cn  12436  hmeores  12473  txswaphmeolem  12478  blfvalps  12543  blgt0  12560  xblss2ps  12562  xblss2  12563  xmetec  12595  bdxmet  12659  bdmopn  12662  metrest  12664  xmetxp  12665  txmetcnp  12676  reopnap  12696  tgioo  12704  divcnap  12713  fsumcncntop  12714  elcncf1ii  12725  cncfmptid  12741  addccncf  12744  cdivcncfap  12745  negcncf  12746  expcncf  12750  cnrehmeocntop  12751  cnopnap  12752  ivthinclemex  12778  limccl  12786  ellimc3apf  12787  limcdifap  12789  limcmpted  12790  cnplimcim  12794  cnplimclemr  12796  limccnpcntop  12802  limccnp2lem  12803  limccnp2cntop  12804  limccoap  12805  reldvg  12806  dvfvalap  12808  dvidlemap  12818  dvcnp2cntop  12821  dvmulxxbr  12824  dvaddxx  12825  dvmulxx  12826  dviaddf  12827  dvimulf  12828  dvcoapbr  12829  dvcjbr  12830  dvcj  12831  dvfre  12832  dvexp  12833  dvrecap  12835  dvmptclx  12838  dvmptcmulcn  12841  dvmptnegcn  12842  dvmptsubcn  12843  dveflem  12844  dvef  12845  sincn  12847  coscn  12848  cosz12  12850  sin0pilem1  12851  sin0pilem2  12852  pilem3  12853  coshalfpip  12892  ptolemy  12894  cosq23lt0  12903  coseq0q4123  12904  coseq00topi  12905  coseq0negpitopi  12906  tangtx  12908  sincos6thpi  12912  cosordlem  12919  cosq34lt1  12920  cos02pilt1  12921  2spim  12962  bj-sbimeh  12968  bj-rspgt  12982  cbvrald  12984  bdsepnft  13074  bj-om  13124  bj-nntrans  13138  bj-nnelirr  13140  setindft  13152  exmid1stab  13184  subctctexmid  13185  nnsf  13188  peano4nninf  13189  peano3nninf  13190  nninfalllemn  13191  nninfsellemcl  13196  nninfself  13198  nninfsellemeq  13199  nninfsellemeqinf  13201  nninffeq  13205  exmidsbthrlem  13206  qdencn  13211  isomninnlem  13214  cvgcmp2nlemabs  13216  cvgcmp2n  13217  trilpolemclim  13218  trilpolemcl  13219  trilpolemisumle  13220  trilpolemgt1  13221  trilpolemeq1  13222  trilpolemlt1  13223  taupi  13228