Theorem a1i 8

Description: Inference derived from axiom ax-1 4. See a1d 15 for an explanation of our informal use of the terms "inference" and "deduction." See also the comment in syld 30.

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 4	. 2 |- (ph -> (ps -> ph))
3	1, 2	ax-mp 7	1 |- (ps -> ph)

Syntax hints:   -> wi 3

This theorem is referenced by:  a1i12 9  imim2i 11  sylOLD 13  mpi 55  mpdi 59  syl9 71  idd 75  pm2.21i 92  pm2.24i 118  pm2.61d1 141  pm2.61d2 142  biidd 187  jctl 312  jctr 313  jctil 314  jctir 315  adantl 422  adantlll 430  sylani 511  sylan2i 512  sylancl 522  sylancr 523  impbid1 572  impbid2 573  syl5bb 588  syl6bb 592  2th 783  biass 813  dedlema 834  dedlemb 836  dedlembOLD 837  dn1 852  3ornot23 1123  bitr3 1125  hbth 1186  19.33b 1282  19.21t 1311  dvelimfALT 1352  cbv3 1363  cbv3ALT 1364  cbvalOLD 1366  sbtOLD 1398  sbie 1403  hbsb4 1458  hbsb4t 1459  sbidmOLD 1466  sbco2 1467  cbvald 1540  sbcom2 1562  dvelimALT 1582  ax11eq 1592  ax11indalem 1597  ax11inda2ALT 1598  a12lem1 1605  eujustALT 1612  eubii 1618  hbeu 1620  mobii 1638  moimv 1652  euor2OLD 1677  2euswap 1686  eqidd 1722  syl5eq 1777  syl6eq 1781  3eqtr4aOLD 1792  syl5eqel 1812  syl5eleq 1814  syl6eqel 1816  syl6eleq 1818  ralbii 1961  rexbii 1962  ralimi 2002  reximi 2032  ralcom2 2078  ralcom2OLD 2079  reubii 2095  hbeqd 2257  hbeld 2258  reu8 2281  sbc8gOLD 2311  cbvsbc 2312  sbcieg 2317  sbcbii 2339  hbsbc1gd 2348  hbsbc1gdOLD 2349  hbsbcgd 2350  hbsbcgdOLD 2351  sbcralt 2360  sbcralgf 2362  hbcsb1gd 2403  hbcsbgd 2404  csbnestglem 2413  csbnest1g 2415  ssconb 2570  reuun1 2698  npss0 2735  tpid3g 2937  difsnOLD 2948  snsspr1OLD 2958  sspr 2966  hbopd 2991  intmin 3059  int0el 3070  eliun 3081  dfiun2 3106  iunab 3121  iunid 3129  iun0 3130  iun0OLD 3131  iinrab 3139  2iunin 3144  syl5breq 3192  ssbri 3199  ssbriOLD 3200  hbbrdOLD 3203  sbcbrgOLD 3209  opabbii 3220  csbopabg 3227  axrep4 3247  axsep 3252  copsexg 3352  dfid3 3402  ordtr2OLD 3524  oneqmini 3529  trsucss 3566  reuuni1 3619  reuuni2f 3621  reuuni2 3622  reuuni4 3624  reusn 3629  reuxfr2d 3655  reuxfr2 3656  reuunixfr 3661  dfwe2 3672  bm2.5ii 3698  suceloni 3705  onuninsuci 3732  nlimsucgOLD 3735  orduninsuc 3736  ordunisuc2 3737  onzslOLD 3740  dflim3 3741  tfinds 3753  dfom2 3762  limom 3778  peano3 3784  peano5 3786  finds1 3793  xpss12 3900  xpss12OLD 3901  relopab 3915  dmcosseq 4025  iss 4065  hbimad 4086  csbima12g 4087  resiima 4093  ssxpb 4157  dfco2 4204  dfco2aOLD 4206  coiun 4218  relssdmrn 4227  unielrel 4229  relfld 4230  funssres 4271  funprg 4277  opabex2 4350  iunfopabOLD 4354  fnopab2 4360  fun 4391  hbfvd 4498  hbfvd2 4499  tz6.12f 4506  csbfv12g 4510  fvelrnb 4530  dfimafn2 4532  fvelimab 4536  fvelimabOLD 4537  fnsnfv 4539  ssimaex 4540  fvopab4g 4553  eqfnfv 4577  elrnopab 4585  fimacnv 4594  fprOLD 4622  fconst4 4638  iunex 4650  funiunfv 4653  cbvfo 4672  isomin 4687  isoini 4688  f1oweALT 4694  hboprdOLD 4717  csboprgOLD 4722  oprabbii 4734  oprabex3 4762  oprabval2gf 4766  oprabval3 4770  oprabval6g 4773  oprvelrn 4780  1stcof 4851  fnoprab2 4875  elrnoprab 4878  fparlem1 4892  fparlem2 4893  fparlem3 4894  fparlem4 4895  fpar 4896  reiotacl 4917  reiota2f 4920  reiota2 4921  onfununi 4927  onopruni 4928  tfrlem4 4933  tz7.49 4979  abianfplem 4981  abianfp 4982  oev2 5018  om0r 5032  oaord 5039  oaordex 5051  oarec 5055  omordi 5056  omord2 5057  oeord 5074  oewordri 5078  oeworde 5079  oelim2 5081  oeoalem 5082  oeoelem 5084  nnaordex 5117  nnawordex 5118  nneob 5123  omsmolem 5124  brecop 5176  mapsspw 5211  mapss 5216  isfi 5252  en2 5272  en3 5273  dom2 5275  fundmen 5298  mapsnen 5299  map1 5300  xpsnen 5305  xpcomen 5309  xpassen 5311  pw2en 5316  ac6sfilem2 5318  ac6sfilem3 5319  ac6sfi 5320  sbthbg 5332  domtriord 5357  canth2 5359  riotaxfrd 5391  mapdom2lem 5397  mapdom2 5398  mapxpen 5399  xpmapenlem5 5404  mapunen 5406  ssenen 5408  phplem4 5415  nneneq 5416  php3 5419  pssnn 5438  unfilem1 5451  unfi 5454  unifi 5458  fiint 5460  iunfi 5469  pwfi 5471  pm54.43 5472  ordiso 5493  ordtypelem6 5499  ordtypelem7 5500  ordtype 5501  hartog 5503  inf0 5521  inf3lem3 5530  inf3lem4 5531  dfom3 5546  infensuc 5554  r1lim 5573  r1ord3 5577  ranksn 5609  rankuni2 5610  rankval4 5622  rankc2 5626  rankxpl 5630  rankxpsuc 5635  19.21a3con13v 5637  tratrb 5640  scott0 5643  cplem1 5646  karden 5652  hta 5654  alephlim 5671  omsubsuc 5673  omsubsuc2 5674  omsubsdomlem1 5675  omsubsdomlem2 5676  omsubsdom 5677  omsubdom 5678  omsubel 5679  omsubss 5680  elomsubsd 5681  omsublim 5683  infenomsub 5685  aceq3lem 5690  aceq5lem4 5696  aceq5lem5 5697  ac6lem 5712  kmlem3 5725  zorn2lem6 5751  zorn2lem7 5752  zorn 5755  fodomb 5758  brdom7disj 5762  brdom6disj 5763  unidom 5766  ficardom 5775  carden 5777  cardlim 5799  cardiun 5807  alephnbtwn2 5813  alephord 5819  alephord3 5822  cardaleph 5829  cardalephex 5830  cardinfima 5835  alephfplem3 5842  alephval3 5847  cfeq0 5858  cfsuc 5859  axextnd 5891  axrepndlem1 5892  axrepndlem2 5893  axunndlem1 5895  axunnd 5896  axpowndlem2 5898  axpowndlem4 5900  axpownd 5901  axregnd 5904  axinfndlem1 5905  axacndlem4 5910  zfcndrep 5914  indpi 5982  ltsopq 6023  prlem934a 6085  prlem936a 6101  reclem4pr 6107  suplem1pr 6109  ltsosr 6151  sqgt0sr 6163  suppsr2 6171  suppsr3 6172  pre-axltadd 6238  pre-axmulgt0 6239  pre-axsup 6240  hbnegd 6314  hbnegdOLD 6315  csbnegg 6316  subaddi 6324  ltxr 6460  lelttr 6489  ltletr 6490  xrlelttr 6533  xrltletr 6534  muleqadd 6685  divmuli 6690  lemul12aOLD 6820  mulgt1 6822  squeeze0 6902  nn1suc 6917  nnleltp1 6933  nnsubi 6935  nnaddm1cl 6937  sup2 7055  dfinfmr 7071  infmsup 7072  xrsupexmnf 7078  xrinfmexpnf 7079  xrsupsslem 7080  xrinfmsslem 7081  xrub 7084  supxrre 7087  supxrmnf 7091  elznn0 7153  nn0sub 7165  zaddcl 7169  zmulcl 7184  zltp1le 7185  dfuzi 7209  uzind 7212  uzind2 7213  uzindOLD 7215  nn0ind 7219  elq 7232  flval3 7274  flhalf 7282  intfracq 7291  iooval2 7329  elioc2 7353  elico2 7354  elicc2 7355  iccf 7365  uzssz 7394  uzind4i 7418  uzwo 7419  uzwoOLD 7420  fzen 7459  fz01en 7460  elfz2nn0 7462  fsequb 7497  om2uzlti 7504  om2uzlt2i 7505  om2uzrani 7506  limsupcl 7568  expm1 7638  expwordi 7643  expubnd 7648  sqlecan 7682  expnbnd 7696  digit1 7700  sqrlem6 7723  sqrlem12 7729  cjreim 7873  cjreim2 7874  leabs 7910  abssubne0 7929  seq1ublem 7958  cau5ii 7964  cvg3i 7970  faclbnd 7992  faclbnd4lem1 7995  faclbnd4lem4 7998  bcn0 8010  bcnp11 8012  fsum1s 8064  fsump1s 8068  fsum1p 8074  fsummulc1 8088  fsumcmp 8095  fsumcmp0 8096  fsumcmpndx2 8097  fsumabs 8098  ser1ser0i 8103  binomlem1 8121  binomlem2 8122  binomlem4 8124  bcxmas 8131  climconsti 8149  climmullem3 8177  climmulc2 8184  iserzshfti 8199  clim2serzi 8200  caucvglem2 8213  caucvg3lem 8221  caucvg3 8223  ser1clim0 8228  cvgcmp2lem 8235  cvgcmpubi 8241  isumclim3 8256  isumnul 8259  arisumi 8282  expcnvlem6 8288  explecnv 8290  geolimilem 8292  georeclim 8297  cvgratlem1ALT 8304  fsum0diag 8315  elcncf1ii 8328  ivthlem6 8343  ivthlem7 8344  efcltlem1 8361  ef0lem 8367  efaddlem2 8396  efaddlem10 8404  efaddlem13 8407  efaddlem15 8409  efaddlem16 8410  efaddlem18 8412  efaddlem19 8413  efaddlem23 8417  efaddlem25 8419  ef01tllem1 8440  ef01tllem2 8441  ef01tllem2OLD 8442  eirrlem2 8447  abspef01tlubi 8455  efcnlem2 8480  efi4p 8495  acdc3lem 8549  acdc4lem1 8551  acdc2lem2 8553  acdc5lem2 8556  infxpidmlem7 8622  infxpidmlem8 8623  infxpdom 8635  infmap2 8645  alephsuc3 8649  fiinbas 8680  subbas2 8710  subtop 8711  indistop 8713  distop 8714  fctop 8715  cctop 8717  iooretop 8724  txbas 8728  iincld 8750  clscld 8754  clsval2 8756  sscls 8760  ntrss2 8761  ssnei 8795  idcn 8837  cnpco 8841  iscncl 8842  cncnplem4 8849  cnconst 8852  sncld 8859  metdmdm 8880  blssm 8922  ssblex 8928  opnfss 8930  opnin 8941  metequiv 8953  tgioolem 8987  dscmet 8991  iscau3 9011  iscau4 9013  caussi 9027  xplmi 9046  fsumcnlem 9062  lmcau 9069  bcthlem8 9079  bcthlem14 9085  bcthlem18 9089  grprlidrid 9132  grpsn 9135  grpidvallem 9136  grpidval 9137  grpidinv2 9139  grpinv 9148  cnid 9230  ga0 9248  gaid 9249  ssga 9250  gapmlem 9256  gapm 9257  vc0 9315  vcm 9317  vsfval 9381  nvm 9389  nvnncan 9410  nvdif 9420  vacnlem3 9464  vacnlem6 9467  nmcn3 9475  nmcnc 9476  sm1cnilem 9481  ipfval 9486  ipval2 9491  ipid 9497  ssps 9523  lno0 9551  nmoxr 9563  nmoge0 9564  nmolb 9568  nmoubi 9569  nmoub3i 9570  nmlnoubi 9591  nmblolbii 9594  isblo3i 9596  blocni 9600  phpar 9619  ubthlem5 9671  minveclem35 9719  minvecdist 9725  htthlem11 9772  pslem 9785  psdmrn 9786  spwval2 9791  spwval3 9792  spwnex3 9793  spwpr4 9801  spwpr4OLD 9802  spwpr4aOLD 9803  spwpr4c 9804  sinperlem1 9830  sinperlem2 9831  coshalfpip 9845  abssinper 9857  efifolem5 9875  eff1o 9897  oprabco 9953  dif1en 9966  fixp 9972  cdrci 9975  clicls 9976  clint3 9977  istoset 10002  fine 10006  tx1cn 10015  tx2cn 10016  upxp 10017  uptx 10018  txcnopab 10020  2txcn 10021  homeofval 10026  hmeobc 10031  subsp 10036  issubsp 10037  subcld 10046  subtopmetlem 10047  subtopmet 10048  oefil2 10067  filfbas 10068  fbssint 10071  infi 10072  fsubbas 10073  fbunfip 10074  elfg 10076  fgfil 10082  extbas1 10083  extbas2 10084  filrn 10085  hausfillim 10095  isfilmap 10100  filmapss 10101  fmf 10102  fmbas 10103  elfilmap 10104  elfilmap3 10106  sflimf 10110  cncomp 10123  usinuniop 10133  dirdm 10146  tosdir 10150  isass 10155  grpmnd 10185  iscom2 10188  on1el3 10204  zrdivrng 10210  hial0 10393  hial02 10394  bcseqi 10411  hlim0 10530  hlimreui 10535  occllem6 10603  occllem7 10604  pjthlem7 10650  pjthlem13 10656  fh1 10986  osumlem3 11007  osumi 11013  hosubid1 11153  honegneg 11161  hoeq2 11186  eigposi 11191  nmopxr 11222  nmfnxr 11235  speccl 11254  hhbloi 11257  nmoplb 11260  nmopub 11261  nmfnlb 11277  nmfnleub 11278  elnlfn2 11282  0cnop 11332  0cnfn 11333  nmopun 11368  nmbdoplbi 11378  nmcopexlem5 11384  nmcoplbi 11387  nmophmi 11390  lnopconi 11392  nmbdfnlbi 11407  nmcfnexlem5 11413  nmcfnlbi 11416  lnfnconi 11419  cnlnadjlem5 11433  cnlnssadj 11442  adjbdln 11445  adjbdlnb 11446  nmopadjlem 11451  adjeq0 11453  nmoptrii 11456  nmopcoi 11457  nmopcoadji 11463  branmfn 11467  branmfnOLD 11468  bra11 11471  kbass2 11480  leop3 11488  leopmul 11497  leopnmid 11501  opsqrlem1 11503  opsqrlem5 11507  opsqrlem6 11508  pjbdlni 11512  staddi 11610  stadd3i 11612  ssmd1 11675  ssmd2 11676  mdslj1i 11683  mdslj2i 11684  mdslmd1lem1 11689  mdslmd1lem2 11690  csmdsymi 11698  elat2 11704  shatomistici 11725  atcvat4i 11761  mdsymlem3 11769  mdsymlem6 11772  mdsymlem8 11774  cdj1i 11797  addltmulALT 11810  bnj927 12627  bnj1024 12671  bnj1141 12731  bnj1207 12773  bnj1213 12778  bnj1252 12809  bnj1261 12812  bnj1262 12813  bnj1263 12815  bnj1464 12935  bnj567 13077  bnj568 13078  bnj889 13115  bnj894 13119  bnj929 13127  bnj1062 13189  bnj1129 13217  bnj1145 13223  bnj1136 13227  bnj1177 13237  bnj1334 13293  bnj1335 13295  bnj1398 13307  bnj1408 13316  bnj1421 13324  bnj1442 13332  bnj1462 13338  bnj1489 13346  bnj1490 13347  bnj1312 13349  bnj1498 13354  bnj1523 13369  ifexg 13391  elnn00nn 13394  elfzp1b 13397  eqreznegel 13446  lbzbi 13449  nn0seqcvgd 13451  nn0seqcvg 13452  absdvdsb 13465  dvdsabsb 13466  dvdslelem 13484  dvdsleabs 13486  divalglem5 13492  gcdcllem1 13510  gcdcllem2 13511  gcdcom 13518  gcdabs 13529  algcvgblem 13537  algcvga 13539  algfx 13540  eucalgval2 13542  eucalgf 13543  eucalglt 13545  truni 13584  trsuc2 13585  fundmpss 13629  dfon2lem6 13645  dfon2lem7 13646  axextdist 13656  axext4dist 13657  distel 13661  elrng 13669  elpred 13679  elpredg 13680  preddowncl 13699  trcllem1 13725  orderseqlem 13745  poseq 13746  soseq 13747  wfrlem10 13758  wfrlem15 13763  elno 13779  nofun 13785  norn 13787  nofv 13790  axsltsolem1 13796  axdenselem4 13812  AiT 13835  TTIid 13844  FTIid 13846  merco2 13933  arg-ax 13970  altdftru 14013  r19.23aivr 14022  alalifal 14055  fnoprvpop 14066  uninqs 14068  infi1 14071  11st22nd 14076  boe 14078  moec 14079  cnvref2 14096  imrescl 14123  imfstnrelc 14126  cmprelid1 14175  eqfnung2 14188  valfunun 14189  surjsec 14191  cmpdom2 14209  mapmapmap 14213  repfuntw 14228  repcpwti 14229  cbcpcp 14230  cbicplem 14234  dstr 14242  iscst4 14248  nZdef 14253  islatalg 14257  domrancur1b 14274  domrancur1c 14276  dupos1 14309  ubos 14321  mnlmxl2 14333  inposet 14344  toplat 14364  dfdir2 14365  fprod1s 14401  fprodp1s 14406  fprod1ib 14410  clfsebs 14430  clfsebsr 14432  fincmpzer 14434  fprodadd 14436  seqzp2 14439  curgrpact 14458  grpdivfo 14460  fprodneg 14464  trdom2 14478  trooo 14481  trinv 14482  cmprtr 14483  rngunval2 14497  isfld 14498  vecval3b 14518  svs2 14552  clsrebb 14567  truni3 14574  oibbi1 14576  oibbi2 14577  nelioo5 14579  clsint 14583  cexint2 14585  sallnei 14594  idhme 14599  hmphsyma 14602  hmphre 14604  hmeogrp 14612  homcard 14613  eqindhome 14615  top2usne 14618  homindlem3 14620  subspemp 14622  subtopsin2 14626  qusp 14627  eltpt 14628  topgele 14629  fgsb 14635  fgsb2 14639  cnfilca 14641  rcfpfil 14648  fbaslim2 14650  limfillem2 14653  dtt2 14665  bwt2 14674  singcon 14682  trhom 14697  altretop 14707  cntrsetlem 14709  msr3 14713  mslb1 14717  2wsms 14718  cnvtr 14726  flimfnein 14729  limnumrr 14730  cinei 14731  flimfneic 14732  flimfneicn 14733  lvsovso2 14735  lvsovso3 14736  1ded 14767  aidm2 14779  1cat 14788  dualcat2lem 14811  dualded2lem 14812  dualalg 14813  dualded 14814  ishomb 14819  ismonc 14845  isepia 14850  isepic 14855  cinvlem2 14859  isfuna 14864  issubcat 14875  issubcata 14876  idsubfun 14888  empistar 14901  tarax3d4 14909  tarsin 14912  tarunpa 14917  cptarc 14924  bpmp 14933  btmp 14934  valtar 14942  vtare 14944  vtarsu 14945  tartarmap 14947  trclval 14953  vtarsuelt 14954  carinttar 14961  isplibg0 14989  isplibg1 14991  isplibg2 14993  isplibg3 14995  isplibg4a 14997  isplibg4b 14999  isplibg 15001  a1i13 15008  a1i14 15010  dmsdtriordOLD 15042  elicc3 15044  finminlem 15049  elfiun 15051  fictblem 15052  fictb 15053  inficlALT 15054  finsschain 15055  ordisoOLD 15056  ordtypelem6OLD 15062  ordtypelem7OLD 15063  ordtypeOLD 15064  hartogOLD 15066  omsubsucOLD 15068  omsubsuc2OLD 15069  omsubsdomlem1OLD 15070  omsubsdomlem2OLD 15071  omsubsdomOLD 15072  omsubdomOLD 15073  omsubelOLD 15074  omsubssOLD 15075  elomsubsdOLD 15076  omsublimOLD 15078  infenomsubOLD 15080  opnbnd 15091  cldbnd 15092  ntrin 15093  cncls 15101  cnntr 15102  subntr 15107  cnsubsp 15108  cnsubsp2 15109  compsublem 15112  compsub 15113  cptclsscpt 15114  hscptsscld 15116  compfipin0lem 15117  compfipin0 15118  alexsublem2 15120  alexsublem3 15121  alexsublem4 15122  connsub 15125  reconnlem1 15128  reconnlem3 15130  reconnlem4 15131  reconnlem5 15132  ivthALT 15136  2ndcsb 15158  2ndc1stc 15159  2ndcctbss 15160  isfne3 15164  ssref 15174  fneerdm 15180  fnessref 15185  refssfne 15186  lfinpfin 15195  locfincomp 15196  locfindsc 15197  locfincf 15198  comppfsc 15199  neibastop1 15200  neibastop2lem1 15201  neibastop3 15206  topmtcl 15207  topjoin 15209  fnemeet1 15210  fnemeet2 15211  fnejoin1 15212  fnejoin2 15213  ist1-2 15224  ist1-3 15225  isnrm2 15234  opnfbas 15239  neifg 15241  supfil 15242  filfinnfr 15243  isufil2 15247  ufprim 15251  filssufillem 15252  filssufil 15253  ufileulem 15254  ufileu 15255  filufint 15256  uffixfr 15257  fixufil 15258  ufinffr 15260  ufilen 15261  filcon 15262  ufcondr 15263  limfilcf 15269  flimcls 15270  cnpfillim 15271  cnfillim 15272  imaelfm 15273  rnelfmlem 15274  rnelfm 15275  fmfnfmlem4 15279  fmfnfm 15280  filfm 15282  sfcls 15286  fcluscf 15294  fclsfnflim 15296  flimfnfcls 15297  fcluscnplem 15299  fcluscomplem 15302  fcluscomp 15303  tailf 15315  istail 15316  tailmap 15318  filnetlem1 15322  filnetlem3 15324  filnetlem4 15325  filnetlem5 15326  filnet 15327  unirep 15346  rabxm 15349  rabnc 15350  prfunOLD 15359  prfOLD 15362  inpreima 15364  unpreima 15365  respreima 15366  fnopabco 15393  cnvcan 15397  upixp 15411  eropreu 15415  abrexdom 15421  abrexdom2 15422  firnfi2 15424  firnfi4 15426  ac6gf 15431  indexa 15435  indexfi 15437  fipreima 15438  inficl 15439  welb 15441  infmrlb 15447  fisup2g 15450  frfi 15453  filbcmb 15458  zmodfzcl 15462  fzfi 15468  fzp1elp1 15476  fzm1 15478  absz 15479  rddif 15480  absrdbnd 15481  absmod0 15484  sdclem1 15491  sdc 15493  fdc 15494  seqpo 15496  incsequz 15497  fsumlt1 15513  csbrni 15514  subspabs 15522  blssp 15526  blhalf 15528  mettrifi 15529  mettrifi2 15530  geomcau 15531  lmclim2 15532  caushft 15533  caures 15534  iccsplit 15536  iccss 15537  iihalf2 15555  iccst 15557  icoopnst 15558  iocopnst 15559  lincmb01cmp 15560  constcncf 15564  addccncf 15565  sub1cncf 15567  sub2cncf 15568  cnimass 15570  cnss 15574  paste 15575  hmeocn 15579  hmeocld 15582  lmtlm 15590  txsubsp 15594  cnopropabcoc 15600  cnoproprabcoc 15602  cnoprab1c 15605  cnoprab2c 15606  sstotbnd 15618  totbndss 15619  isbnd3 15623  totbndbnd 15626  ismtycnv 15631  ismtyres 15636  heiborlem1 15637  heiborlem6 15642  heiborlem9 15645  heiborlem10 15646  heiborlem11 15647  heiborlem12 15648  heiborlem13 15649  heiborlem14 15650  heiborlem15 15651  heiborlem16 15652  heiborlem28 15664  heiborlem32 15668  heiborlem33 15669  heiborlem34 15670  heiborlem35 15671  heiborlem36 15672  heiborlem39 15675  heiborlem42 15678  bfplem3 15682  bfplem6 15685  bfplem7 15686  bfplem8 15687  bfplem11 15690  bfp 15691  recms 15692  rrndm 15697  rrndstprj2 15700  rrncms 15701  rrntotbndlem1 15702  rrntotbndlem2 15703  rrntotbnd 15704  ismrer1 15706  reheibor 15707  iccbnd 15708  exidresid 15714  ghomco 15722  phtpyfval 15728  phtpyval 15729  phtpyid 15731  phtpycom 15732  phtpycolem2 15734  phtpycolem3 15735  phtpycolem4 15736  phtpycolem5 15737  reparphtlem2 15746  reparpht 15747  pcocn 15758  pcoloopf 15761  pcohtpylem3 15764  pcopt 15766  pcoass 15767  pcorevlem 15768  pcorev 15769  pi1bval 15770  pi1bvalqs 15773  pi1f 15775  pi1val 15776  pi1gp 15777  isdivrng2 15793  rngidl 15854  0idl 15855  smprngpr 15882  prnc 15897  isdmn3 15904  prtlem60 15908  jca2 15913  jca2r 15914  prtlem50 15916  ax10-16 16047  dvelimfALT2 16048  fveqsb 16113  smores 16128  smoge 16136  vd01 16156  vd02 16157  vd03 16158  idn3 16168  ee202 16188  ee022 16190  ee002 16192  ee020 16194  ee200 16196  ee210 16208  ee201 16210  ee120 16212  ee021 16214  ee012 16216  ee102 16218  e22 16219  ee110 16224  ee101 16226  ee011 16228  ee100 16230  ee010 16232  ee001 16234  e11 16235  ee11 16236  ee01 16240  ee10 16244  ee02 16248  e33 16262  e3 16266  ee03 16270  ee30 16274  sspwtrALT2 16304  pwtr 16306  pwtrr 16308  suctrALT2 16320  strssp1 16472  stbcl 16489  lubprop 16563  glbprop 16568  joincomALT 16586  meetcomALT 16588  p0le 16603  ple1 16604  lublem 16651  cmtbr2 16724  hlatmstc 16790  hlrelat2 16793  cvrat4 16806  grpidinv2NEW 16848  grpinvNEW 16857  isline 16949  ispoint 16951  ispsubsp2 16955  linepsub 16960  atpsub 16961  pmapssat 16966  pmap0 16969  pmapglb 16972  pluspunss 16982  elplusp0 16983  plusp01 16985  plusp02 16986  pluspcom 16987  ssplusp1 16989  ssplusp2 16990  paddidm 17014

This theorem was proved from axioms:  ax-1 4  ax-mp 7

Copyright terms: Public domain