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  1897  cbvexdh  1898  nfsbxy  1915  sbcomxyyz  1945  dvelimALT  1985  dvelimfv  1986  hbsb4t  1988  dvelimor  1993  eubii  2008  nfeudv  2014  nfmo  2019  mobii  2036  moimv  2065  2euswapdc  2090  eqidd  2140  syl5eq  2184  syl6eq  2188  eqeltrid  2226  eleqtrid  2228  eqeltrdi  2230  eleqtrdi  2232  nfcvd  2282  dvelimc  2302  nnedc  2313  necon1idc  2361  ralbii  2441  rexbii  2442  nfraldxy  2467  nfrexdxy  2468  nfralxy  2471  nfrexxy  2472  nfralya  2473  nfrexya  2474  rgenw  2487  ralimi  2495  rexim  2526  reximi  2529  rexlimivw  2545  r19.29af2  2572  r19.32vdc  2580  nfreudxy  2604  nfreuxy  2605  reubii  2616  rmobii  2621  rabbii  2672  ceqsralt  2713  vtoclgft  2736  rr19.28v  2824  reu8  2880  cdeqth  2896  nfsbc1d  2925  nfsbc1  2926  nfsbc  2929  sbcbii  2968  sbc2iegf  2979  sbc2iedv  2981  sbc3ie  2982  sbcrext  2986  rmob  3001  sbcnel12g  3019  sbcne12g  3020  csbcomg  3025  csbeq2i  3029  nfcsb1  3034  nfcsb  3037  csbiebt  3039  csbief  3044  csbie2t  3048  sbcnestgf  3051  sstrid  3108  sstrdi  3109  ssidd  3118  sseqtrrid  3148  eqsstrdi  3149  difssd  3203  ssconb  3209  abvor0dc  3386  rabnc  3395  nfif  3500  disjpr2  3587  tpid3g  3638  neldifsnd  3654  diftpsn3  3661  preq12bg  3700  intmin  3791  int0el  3801  dfiun2  3847  dfiin2  3848  dfiunv2  3849  iunrab  3860  iunid  3868  iun0  3869  iinrabm  3875  iunin1  3877  2iunin  3879  iinin1m  3882  breqtrid  3965  ssbri  3972  nfbr  3974  opabbii  3995  mpteq2i  4015  mpteq12i  4016  opth1  4158  copsexg  4166  copsex4g  4169  epelg  4212  issod  4241  fr0  4273  frind  4274  trsucss  4345  bm2.5ii  4412  ordsucss  4420  onsucelsucr  4424  ordunisuc2r  4430  ordirr  4457  ordfr  4489  peano5  4512  finds1  4516  ordom  4520  0elnn  4532  omsinds  4535  0nelrel  4585  csbcnvg  4723  dfiun3  4798  dfiin3  4799  dmcosseq  4810  resiun1  4838  resiun2  4839  resima2  4853  iss  4865  resiima  4897  relbrcnvg  4918  inimasn  4956  elxp4  5026  elxp5  5027  dfco2  5038  coiun  5048  relssdmrn  5059  unielrel  5066  relfld  5067  cnviinm  5080  cnvsom  5082  nfiotadw  5091  nfiotaw  5092  iota2df  5112  funssres  5165  fntp  5180  imadif  5203  imain  5205  sbcfng  5270  sbcfg  5271  fun  5295  fun11iun  5388  funcocnv2  5392  f1oprg  5411  sefvex  5442  tz6.12f  5450  dfimafn2  5471  fnsnfv  5480  ssimaex  5482  fvun1  5487  fvmptg  5497  fvmpt3i  5501  fvopab6  5517  fndmdifcom  5526  respreima  5548  fmptco  5586  fcoconst  5591  dfmpt  5597  fmptapd  5611  fmptpr  5612  isocnv2  5713  riotaexg  5734  nfriotadxy  5738  nfriota  5739  riota2f  5751  nfov  5801  oprabbii  5826  mpoeq123i  5834  ovmpt4g  5893  ovmpodxf  5896  ovmpox  5899  ovmpoga  5900  ovi3  5907  ov6g  5908  ovelrn  5919  caovcom  5928  caovass  5931  caovdi  5950  caovimo  5964  ofc12  6002  oprabex3  6027  reldm  6084  fnmpoovd  6112  oprabco  6114  oprab2co  6115  disjsnxp  6134  mpoxopoveq  6137  brtpos2  6148  reldmtpos  6150  dmtpos  6153  dftpos4  6160  tposfn2  6163  smores  6189  tfrlemisucfn  6221  tfrlemiubacc  6227  tfri1dALT  6248  tfrcl  6261  tfri1  6262  rdgon  6283  frec0g  6294  frectfr  6297  freccllem  6299  frecfcllem  6301  frecsuclem  6303  oacl  6356  omcl  6357  oeicl  6358  oawordi  6365  nnsucelsuc  6387  nntri1  6392  nnsseleq  6397  nnaord  6405  nnmordi  6412  nnmord  6413  nnaordex  6423  nnm00  6425  swoer  6457  eqer  6461  0er  6463  uniqs  6487  erinxp  6503  qliftf  6514  brecop  6519  ecopovtrn  6526  ecopover  6527  ecopoverg  6530  th3qlem1  6531  elpmg  6558  nfixpxy  6611  ixpintm  6619  ixpsnf1o  6630  brdomg  6642  en2i  6664  en3i  6665  dom2  6669  dom3  6670  ener  6673  ensymb  6674  entr  6678  fundmen  6700  mapsnen  6705  map1  6706  enpr2d  6711  xpsnen  6715  xpassen  6724  ssenen  6745  nneneq  6751  phplem4dom  6756  phpelm  6760  phplem4on  6761  fidceq  6763  fiunsnnn  6775  finexdc  6796  infm  6798  exmidpw  6802  unfidisj  6810  undifdc  6812  unfiin  6814  fiintim  6817  xpfi  6818  fisseneq  6820  ssfirab  6822  fnfi  6825  iunfidisj  6834  f1finf1o  6835  fidcenumlemrk  6842  fidcenumlemr  6843  elfi2  6860  ssfii  6862  supubti  6886  suplubti  6887  cnvinfex  6905  eqinfti  6907  infvalti  6909  inflbti  6911  ordiso2  6920  djuex  6928  inl11  6950  djuss  6955  1stinl  6959  2ndinl  6960  1stinr  6961  2ndinr  6962  updjudhcoinlf  6965  updjudhcoinrg  6966  casefun  6970  caseinl  6976  caseinr  6977  omp1eomlem  6979  endjusym  6981  difinfsn  6985  djufun  6989  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  finomni  7012  fodjuomnilemdc  7016  fodjuf  7017  fodjum  7018  fodju0  7019  nnnninf  7023  ctssexmid  7024  ismkvnex  7029  omnimkv  7030  mkvprop  7032  cardcl  7037  pm54.43  7046  en2other2  7052  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  acfun  7063  exmidaclem  7064  endjudisj  7066  djuen  7067  djuassen  7073  xpdjuen  7074  ccfunen  7079  elni2  7122  indpi  7150  enqeceq  7167  mulcanenqec  7194  ltnnnq  7231  enq0er  7243  enq0eceq  7245  nqnq0pi  7246  mulcanenq0ec  7253  nnnq0lem1  7254  addnq0mo  7255  mulnq0mo  7256  prarloclemlo  7302  prarloclem3  7305  genipv  7317  nqprrnd  7351  nqprdisj  7352  nqprloc  7353  1idprl  7398  1idpru  7399  recexprlemlol  7434  recexprlemupu  7436  cauappcvgprlemm  7453  cauappcvgprlemdisj  7459  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgpr  7470  caucvgprlemm  7476  caucvgprlemcl  7484  caucvgprlemladdrl  7486  caucvgpr  7490  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemopu  7507  caucvgprprlemclphr  7513  suplocexprlemss  7523  suplocexprlemlub  7532  enreceq  7544  prsrlem1  7550  addsrmo  7551  mulsrmo  7552  0idsr  7575  pn0sr  7579  recexgt0sr  7581  archsr  7590  srpospr  7591  prsradd  7594  prsrlt  7595  caucvgsrlemfv  7599  caucvgsrlembound  7602  caucvgsrlemoffval  7604  caucvgsrlemoffcau  7606  caucvgsrlemoffgt1  7607  caucvgsrlemoffres  7608  caucvgsr  7610  ltpsrprg  7611  mappsrprg  7612  map2psrprg  7613  suplocsrlemb  7614  pitonnlem1p1  7654  pitoregt0  7657  recidpirqlemcalc  7665  recidpirq  7666  axcnex  7667  axmulcl  7674  axmulass  7681  axdistr  7682  ax0id  7686  axprecex  7688  axpre-ltirr  7690  axpre-lttrn  7692  axpre-ltadd  7694  axpre-mulgt0  7695  axpre-mulext  7696  axcaucvglemval  7705  axcaucvg  7708  0cnd  7759  0red  7767  1red  7781  1cnd  7782  ltxrlt  7830  1p1times  7896  nfneg  7959  negsub  8010  addlsub  8132  pncan1  8139  npcan1  8140  negf1o  8144  kcnktkm1cn  8145  mulsubfacd  8180  rereim  8348  cru  8364  apreim  8365  mulreim  8366  apadd1  8370  apneg  8373  aprcl  8408  muleqadd  8429  eqneg  8492  mulgt1  8621  suprlubex  8710  negiso  8713  dfinfre  8714  sup3exmid  8715  cju  8719  nn1suc  8739  2cnd  8793  avglt1  8958  avglt2  8959  add1p1  8969  sub1m1  8970  cnm2m1cnm3  8971  xp1d2m1eqxm1d2  8972  div4p1lem1div2  8973  nn0p1gt0  9006  un0addcl  9010  nn0ge2m1nn  9037  0zd  9066  elnn0z  9067  elznn0  9069  1zzd  9081  peano2z  9090  ztri3or0  9096  zlelttric  9099  zltnle  9100  zmulcl  9107  zltp1le  9108  zgt0ge1  9112  elz2  9122  zdceq  9126  zdclt  9128  nn0lt2  9132  nn0le2is012  9133  zneo  9152  nneo  9154  zeo2  9157  uzind  9162  uzind2  9163  nn0ind  9165  zadd2cl  9180  uzm1  9356  uzin  9358  uz3m2nn  9368  uzind4i  9387  infrenegsupex  9389  supminfex  9392  eqreznegel  9406  nn01to3  9409  nn0ge2m1nnALT  9410  divfnzn  9413  cnref1o  9440  rpnegap  9474  divlt1lt  9511  divle1le  9512  ltxr  9562  xrre3  9605  xaddf  9627  xaddval  9628  xaddnemnf  9640  xaddnepnf  9641  xaddass2  9653  xltadd1  9659  xaddge0  9661  xlt2add  9663  xleaddadd  9670  ixxssixx  9685  elioc2  9719  elico2  9720  elicc2  9721  lincmb01cmp  9786  fzdcel  9820  ige3m2fz  9829  fz01en  9833  fzdifsuc  9861  elfz1b  9870  uzsplit  9872  fseq1p1m1  9874  elfzp1b  9877  ige2m1fz1  9889  ige2m1fz  9890  0elfz  9898  fz0tp  9901  fz0fzdiffz0  9907  nn0split  9913  nnsplit  9914  fzoval  9925  fzouzsplit  9956  elfzom1elp1fzo  9979  elfzonlteqm1  9987  fzo0to3tp  9996  fzo0sn0fzo1  9998  fzosplitprm1  10011  fvinim0ffz  10018  qlelttric  10022  qltnle  10023  qdceq  10024  qbtwnrelemcalc  10033  qbtwnre  10034  ioo0  10037  ioom  10038  ico0  10039  ioc0  10040  2tnp1ge0ge0  10074  flhalf  10075  fldiv4p1lem1div2  10078  intfracq  10093  q0mod  10128  q1mod  10129  mulp1mod1  10138  modqnegd  10152  modsumfzodifsn  10169  frec2uzltd  10176  frec2uzlt2d  10177  frecfzennn  10199  uzennn  10209  1tonninf  10213  iseqvalcbv  10230  seq3val  10231  seqvalcd  10232  seq3-1  10233  seqf  10234  seq3p1  10235  seqf2  10237  seq1cd  10238  seqp1cd  10239  seq3clss  10240  monoord  10249  seq3caopr3  10254  seq3f1olemp  10275  seq3id3  10280  seq3homo  10283  seq3z  10284  ser0  10287  ser3ge0  10290  exp0  10297  expgt1  10331  ltexp2a  10345  leexp2a  10346  leexp2r  10347  exple1  10349  expubnd  10350  binom21  10404  binom2sub1  10406  zesq  10410  expnlbnd2  10417  sqeq0d  10423  sqoddm1div8  10444  expcanlem  10462  expcan  10463  nn0opthlem1d  10466  nn0opthlem2d  10467  faclbnd  10487  faclbnd2  10488  bc0k  10502  bcn1  10504  bcn2  10510  bcn2m1  10515  bcn2p1  10516  fihashen1  10545  hashunlem  10550  1elfz0hash  10552  hashprg  10554  hashdifpr  10566  hashxp  10572  zfz1isolem1  10583  seq3coll  10585  shftuz  10589  ovshftex  10591  shftfn  10596  imval  10622  crre  10629  crim  10630  remim  10632  cjreb  10638  readd  10641  remullem  10643  imadd  10649  cjadd  10656  cjreim  10675  cjreim2  10676  cjap  10678  cnrecnv  10682  cvg1nlemcxze  10754  cvg1nlemres  10757  rexfiuz  10761  r19.29uz  10764  resqrexlem1arp  10777  resqrexlemfp1  10781  resqrexlemover  10782  resqrexlemdec  10783  resqrexlemdecn  10784  resqrexlemlo  10785  resqrexlemcalc1  10786  resqrexlemcalc2  10787  resqrexlemcalc3  10788  resqrexlemnmsq  10789  resqrexlemnm  10790  resqrexlemcvg  10791  resqrexlemglsq  10794  resqrexlemga  10795  resqrexlemsqa  10796  sqrtgt0  10806  sqrtsq  10816  absimle  10856  abstri  10876  cau3lem  10886  amgm2  10890  maxabsle  10976  maxabslemab  10978  maxabslemlub  10979  maxltsup  10990  max0addsup  10991  fimaxre2  10998  minabs  11007  bdtrilem  11010  bdtri  11011  xrmaxiflemcl  11014  xrmaxiflemcom  11018  xrmaxadd  11030  infxrnegsupex  11032  xrbdtri  11045  clim  11050  climshft  11073  climle  11103  clim2ser  11106  clim2ser2  11107  iserex  11108  isermulc2  11109  climrecvg1n  11117  climcvg1nlem  11118  climcaucn  11120  sumrbdclem  11146  fsum3cvg  11147  summodclem2a  11150  sum0  11157  fisumss  11161  fsumrecl  11170  fsumzcl  11171  fsumnn0cl  11172  fsumrpcl  11173  fsumadd  11175  fsumsplitf  11177  sumsnf  11178  sumpr  11182  sumtp  11183  isumclim3  11192  isumadd  11200  sumsplitdc  11201  fsum2dlemstep  11203  fisumcom2  11207  fsumcom  11208  fisum0diag  11210  fisum0diag2  11216  fsumneg  11220  fsumconst  11223  modfsummodlemstep  11226  modfsummod  11227  fsumge0  11228  fsumlessfi  11229  fsumabs  11234  fsumrelem  11240  iserabs  11244  fsumiun  11246  hash2iun1dif1  11249  binomlem  11252  isumshft  11259  isumnn0nn  11262  isumlessdc  11265  divcnv  11266  trireciplem  11269  trirecip  11270  expcnvap0  11271  expcnvre  11272  expcnv  11273  explecnv  11274  geosergap  11275  geoserap  11276  geolim  11280  georeclim  11282  geo2sum  11283  geo2sum2  11284  geo2lim  11285  geoisumr  11287  geoisum1  11288  geoisum1c  11289  0.999...  11290  geoihalfsum  11291  cvgratnnlembern  11292  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratnnlemsumlt  11297  cvgratnnlemfm  11298  cvgratnnlemrate  11299  cvgratnn  11300  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  clim2prod  11308  clim2divap  11309  prodf1  11311  prodfrecap  11315  prodrbdclem  11340  fproddccvg  11341  prodmodclem2a  11345  efcllemp  11364  efcllem  11365  ef0lem  11366  ege2le3  11377  efcj  11379  efgt0  11390  eftlub  11396  efsep  11397  ef4p  11400  efgt1p2  11401  efgt1p  11402  sinval  11409  cosval  11410  tanval2ap  11420  tanval3ap  11421  efi4p  11424  sinadd  11443  cosadd  11444  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  sin01gt0  11468  cos12dec  11474  eirraplem  11483  nndivdvds  11499  absdvdsb  11511  dvdsabsb  11512  dvds1  11551  dvdsfac  11558  zeneo  11568  odd2np1lem  11569  even2n  11571  oexpneg  11574  oddge22np1  11578  evennn02n  11579  evennn2n  11580  2tp1odd  11581  mulsucdiv2z  11582  ltoddhalfle  11590  halfleoddlt  11591  m1expo  11597  m1exp1  11598  nn0enne  11599  nn0ehalf  11600  nn0o1gt2  11602  nno  11603  nn0o  11604  nn0oddm1d2  11606  nnoddm1d2  11607  4dvdseven  11614  flodddiv4  11631  flodddiv4lt  11633  flodddiv4t2lthalf  11634  zsupcllemex  11639  zsupcl  11640  infssuzex  11642  infssuzcldc  11644  gcddvds  11652  zeqzmulgcd  11659  gcdcom  11662  gcdabs  11676  gcdabs1  11677  dfgcd3  11698  gcdass  11703  bezoutr1  11721  nn0seqcvgd  11722  alginv  11728  algcvg  11729  algcvga  11732  algfx  11733  eucalgcvga  11739  eucalg  11740  lcmval  11744  lcmcom  11745  lcmabs  11757  lcmass  11766  ncoprmgcdne1b  11770  cncongr1  11784  prmind2  11801  dvdsnprmd  11806  prmgt1  11812  oddprmge3  11815  coprm  11822  sqrt2irrlem  11839  sqrt2irr  11840  sqrt2irr0  11842  pw2dvdslemn  11843  pw2dvdseulemle  11845  oddpwdclemxy  11847  oddpwdclemodd  11850  oddpwdclemdc  11851  oddpwdc  11852  sqpweven  11853  2sqpwodd  11854  sqrt2irraplemnn  11857  sqrt2irrap  11858  divdenle  11875  nn0gcdsq  11878  numdensq  11880  nn0sqrtelqelz  11884  dfphi2  11896  phimullem  11901  oddennn  11905  evenennn  11906  unennn  11910  ennnfonelemj0  11914  ennnfonelemg  11916  ennnfonelemh  11917  ennnfonelemp1  11919  ennnfonelem1  11920  ennnfonelemhdmp1  11922  ennnfonelemss  11923  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemrn  11932  ennnfonelemnn0  11935  ctinfomlemom  11940  ctinf  11943  ctiunctlemuom  11949  ctiunct  11953  unct  11954  structcnvcnv  11975  strnfvn  11980  strndxid  11987  fvsetsid  11993  setsfun  11994  setsfun0  11995  setscom  11999  strslfvd  12000  strslfv2d  12001  strslfv2  12002  strslfv  12003  strslss  12006  setsslid  12009  setsslnid  12010  ressval2  12019  ressid  12020  strle1g  12049  strle2g  12050  strle3g  12051  2strbasg  12060  2stropg  12061  srngstrd  12081  lmodstrd  12092  ipsstrd  12100  istopon  12180  fiinbas  12216  baspartn  12217  eltg4i  12224  bastg  12230  unitg  12231  tgdom  12241  tgidm  12243  distop  12254  distopon  12256  epttop  12259  isopn3  12294  tgrest  12338  resttopon  12340  restin  12345  rest0  12348  lmfval  12361  cnfval  12363  cnpfval  12364  cnrest2  12405  cnrest2r  12406  cnptopresti  12407  cnptoprest  12408  cnptoprest2  12409  lmres  12417  txbasval  12436  tx1cn  12438  tx2cn  12439  txcnp  12440  txrest  12445  txdis1cn  12447  hmeores  12484  txswaphmeolem  12489  blfvalps  12554  blgt0  12571  xblss2ps  12573  xblss2  12574  xmetec  12606  bdxmet  12670  bdmopn  12673  metrest  12675  xmetxp  12676  txmetcnp  12687  reopnap  12707  tgioo  12715  divcnap  12724  fsumcncntop  12725  elcncf1ii  12736  cncfmptid  12752  addccncf  12755  cdivcncfap  12756  negcncf  12757  expcncf  12761  cnrehmeocntop  12762  cnopnap  12763  ivthinclemex  12789  limccl  12797  ellimc3apf  12798  limcdifap  12800  limcmpted  12801  cnplimcim  12805  cnplimclemr  12807  limccnpcntop  12813  limccnp2lem  12814  limccnp2cntop  12815  limccoap  12816  reldvg  12817  dvfvalap  12819  dvidlemap  12829  dvcnp2cntop  12832  dvmulxxbr  12835  dvaddxx  12836  dvmulxx  12837  dviaddf  12838  dvimulf  12839  dvcoapbr  12840  dvcjbr  12841  dvcj  12842  dvfre  12843  dvexp  12844  dvrecap  12846  dvmptclx  12849  dvmptcmulcn  12852  dvmptnegcn  12853  dvmptsubcn  12854  dveflem  12855  dvef  12856  sincn  12858  coscn  12859  cosz12  12861  sin0pilem1  12862  sin0pilem2  12863  pilem3  12864  coshalfpip  12903  ptolemy  12905  cosq23lt0  12914  coseq0q4123  12915  coseq00topi  12916  coseq0negpitopi  12917  tangtx  12919  sincos6thpi  12923  cosordlem  12930  cosq34lt1  12931  cos02pilt1  12932  2spim  12973  bj-sbimeh  12979  bj-rspgt  12993  cbvrald  12995  bdsepnft  13085  bj-om  13135  bj-nntrans  13149  bj-nnelirr  13151  setindft  13163  exmid1stab  13195  subctctexmid  13196  nnsf  13199  peano4nninf  13200  peano3nninf  13201  nninfalllemn  13202  nninfsellemcl  13207  nninfself  13209  nninfsellemeq  13210  nninfsellemeqinf  13212  nninffeq  13216  exmidsbthrlem  13217  qdencn  13222  isomninnlem  13225  cvgcmp2nlemabs  13227  cvgcmp2n  13228  trilpolemclim  13229  trilpolemcl  13230  trilpolemisumle  13231  trilpolemgt1  13232  trilpolemeq1  13233  trilpolemlt1  13234  taupi  13239