Theorem imp 377

Description: Importation inference. (The proof was shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis

Ref	Expression
imp.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
imp	|- ((ph /\ ps) -> ch)

Proof of Theorem imp

Step	Hyp	Ref	Expression
1		imp.1	. 2 |- (ph -> (ps -> ch))
2		impexp 374	. 2 |- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))
3	1, 2	mpbir 207	1 |- ((ph /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  impcom 378  pm3.33 384  pm3.34 385  pm3.35 386  pm5.31 387  imp31 389  imp32 390  imp4b 392  imp41 395  imp42 396  imp43 397  imp44 398  imp45 399  imp5a 400  expdimp 406  expr 418  impac 423  adantl 424  adantr 425  adantll 428  adantlr 429  adantrl 430  adantrr 431  biimpa 460  biimpar 461  biimpac 462  biimparc 463  jaob 467  jaoian 470  jaodan 471  pm4.43 477  imdistani 491  sylan 497  sylan2 500  syldan 516  sylan9 517  sylan9r 519  anabsi7 555  3imtr3g 611  ordiOLD 657  jcad 661  orcanai 754  mpanl1 770  mpanl2OLD 772  mpanr1OLD 775  mpanr2OLD 777  mpanlr1 779  pm4.82 811  consensus 844  dn1 855  dn1OLD 856  3adantl1 1032  3adantl2 1033  3adantl3 1034  3jcad 1051  3expia 1069  3an1rs 1080  3imp1 1081  3imp2 1083  syl3anl1 1145  syl3anl2 1146  syl3anl3 1147  3anidm12 1154  3anidm23 1156  3jaoian 1162  3jaodan 1163  mp3anl1 1185  mp3anl2 1186  mp3anl3 1187  meredith 1200  ee222 1271  alanimi 1342  19.21adOLD 1407  19.26 1416  19.29 1421  equtr2OLD 1493  equs4 1510  dvelimfALT 1514  a4imt 1519  a4imed 1522  equvini 1531  equviniOLD 1532  equs5a 1566  ax11v2 1585  ax11b 1590  dfsb2 1595  hbsb4 1620  dvelimdf 1624  sbcom 1632  sb5rf 1633  equvin 1652  dvelimALT 1744  ax11eq 1754  ax11el 1755  ax11indi 1758  ax11indalem 1759  ax11inda2ALT 1760  ax11inda 1762  a12stdy2 1764  a12lem1 1767  mopick 1833  moexex 1841  exists2 1863  eqrdav 1883  nelneq 1985  nelneq2 1986  pm13.18 2085  nelne 2100  r19.21advv 2184  r19.21bi 2188  r19.23aiOLD 2210  r19.26 2219  ralbi 2223  r19.29 2227  rcla4va 2378  elabgt 2400  euind 2439  reu6 2443  reuind 2450  ra4sbca 2537  ra4esbca 2538  csbexg 2548  ra4csbela 2587  ssel2 2616  sstr 2625  sspsstr 2715  psssstr 2716  neldif 2733  rabbirdv 2801  reuss2 2870  reupick 2874  reximdva0 2886  ssn0 2905  ssdisj 2923  disjpss 2924  disjssunOLD 2933  pssdifn0 2936  dedth2h 3015  dedth4h 3017  sspr 3144  prel12 3155  uniintsn 3253  iineq2OLD 3275  dfiun2g 3283  ssiunOLD 3294  dtru 3498  pwssun 3578  poirr 3597  potr 3598  frirr 3634  wefrc 3652  wereu 3654  ordelss 3674  trssord 3675  nordeq 3677  ordelord 3680  tz7.7 3684  onfr 3702  ordtr2OLD 3709  limelon 3727  trsuc 3752  trsucOLD 3753  ordsssuc2OLD 3759  unizlim 3786  reuuni2f 3810  mouniss 3816  rabxfrd 3842  elpwunsn 3856  oninton 3881  limuni3 3936  tfi 3937  tfindsOLD 3943  tfindsg 3944  tfindsg2 3945  limomss 3956  ordom 3960  ordomOLD 3961  peano5 3975  findsg 3980  brrelex 4028  optocl 4061  elrel 4086  relop 4113  opelxpex2 4119  opelxpex2OLD 4120  breldmg 4162  elreldm 4185  relimasn 4288  asymref2OLD 4311  funeu 4444  funopg 4454  funssres 4460  fununi 4481  funimass2 4492  fneuOLD 4518  fnun 4520  fssOLD 4572  fco 4573  fcoOLD 4574  opelf 4579  f1oun 4658  f1dmex 4664  fv3 4690  nfunsnOLD 4707  funopfvg 4711  fvelimaOLD 4724  fvelimabOLD 4726  fvco 4736  fvco2OLD 4738  fvopab3ig 4741  elrnopabg 4773  dff3 4790  funfvima2 4829  funfvima3 4830  isorel 4871  isocnv 4873  isotr 4874  isotrALT 4875  isomin 4876  isoini 4877  isofrlem 4878  f1oweALT 4883  ndmoprcl 4977  1stdm 5049  reiota2f 5109  onfununi 5116  onopriun 5118  tfrlem2 5120  tfrlem7 5125  tfrlem8 5126  tfrlem9 5127  tfrlem11 5129  tfr3 5134  rdglim 5156  tz7.49 5168  abianfp 5171  oevn0 5199  oaordi 5227  oawordeu 5237  oawordexr 5238  oalimcl 5242  oaass 5243  oarec 5244  omordi 5245  omcan 5248  omwordri 5251  omword1 5252  omlimcl 5257  odi 5258  omass 5259  oecan 5264  oewordi 5266  oewordri 5267  oeordsuc 5269  oeoa 5272  oeoe 5274  nnacom 5288  nnmcom 5297  nnmcomOLD 5298  oaabs 5309  omsmolem 5313  omsmo 5314  eceqopreq 5372  th3qlem1 5373  th3qlem2 5374  f1oen2g 5453  en3d 5460  dom2d 5463  fundmen 5487  undom 5497  xpdom2 5501  pw2en 5505  ac6sfilem3 5508  ac6sfi 5509  sbthlem1 5510  ensdomtr 5534  domsdomtr 5539  enen1 5540  enen2 5541  domen1 5542  domen2 5543  sdomen1 5544  sdomen2 5545  riotabidva 5575  riota5 5580  riotaxfrd 5581  mapenlem2 5584  mapen 5585  mapdom2 5588  mapunen 5596  nneneq 5606  php 5607  php3 5609  finsucdom 5620  pssinf 5621  isfinite1 5624  infsdomnn 5625  pssnn 5628  ssfi 5630  domfi 5631  unblem3 5635  unfilem1 5641  unifi 5648  fiint 5650  abfii4 5654  fodomfi 5656  fodomfib 5657  iunfi 5659  pm54.43 5662  supmo 5666  suppr 5680  ordiso 5683  ordtypelem4 5687  ordtypelem6 5689  ordtypelem7 5690  ordtype 5691  hartog 5693  suc11reg 5710  inf3lem1 5719  inf3lem5 5723  unbnn3 5746  zfregs 5754  setind 5759  r1ord 5766  r1val1 5769  tz9.12lem3 5772  rankr1 5785  ssrankr1 5787  rankxplim3 5825  rankxpsuc 5826  omsubsuc2 5878  omsubsdomlem2 5880  omsubsdom 5881  omsubel 5883  omsubindss 5888  infenomsub 5889  aceq3 5895  aceq5lem4 5900  aceq5 5902  aceq6b 5904  ac6s 5918  numthlem 5945  zorn2lem1 5950  zorn2lem4 5953  zorn2lem5 5954  zorn2lem6 5955  zorn2lem7 5956  fodomb 5962  unidom 5970  uniimadom 5972  unxpdomlem 5995  cardlim 6003  ondomon 6008  carduni 6010  alephordi 6022  alephle 6032  cardaleph 6033  cardinfima 6039  alephval3 6051  cflim 6057  axrepndlem1 6096  axrepndlem2 6097  axrepnd 6098  axpowndlem4 6104  axinfndlem1 6109  axacndlem4 6114  axacndlem5 6115  axacnd 6116  mulclpi 6173  mulcanpi 6179  ltmpi 6183  indpi 6186  ltaddpq 6231  elprpq 6247  prcdpq 6249  distrlem4pr 6282  psslinpr 6287  prlem934a 6289  prlem934 6291  ltaddpr 6292  ltexprlem3 6296  ltexprlem5 6298  ltaprlem 6302  prlem936 6307  suplem1pr 6313  mulcmpblnr 6335  recexsrlem 6364  mulgt0sr 6366  ssgt0sr 6369  suppsrlem 6373  suppsr2 6375  suppsr3 6376  suprelem 6411  axrrecex 6437  cnegexlem1 6499  cnegexlem2 6500  addcaniOLD 6506  renegcliOLD 6577  mulgt0 6678  xrre 6744  xrre2 6745  addgegt0iOLD 6780  msqgt0 6797  gt0ne0 6800  addgt0 6831  addgt0OLD 6832  addgegt0 6833  addgegt0OLD 6834  addgtge0 6835  addge0 6837  addge0OLD 6838  mulge0 6868  mulge0OLD 6869  recex 6876  mulcani 6878  recne0 6915  recid 6918  redivcli 6976  prodgt0i 6997  prodge0i 6998  prodgt0 7004  prodgt02 7005  prodge0 7006  prodge02 7007  lemul1OLD 7012  ltmul12a 7023  lemul12aOLD 7025  mulgt1 7027  ltdiv1OLD 7032  lediv1OLD 7034  ltmuldivOLD 7046  ltmuldiv2OLD 7048  ltdivmulOLD 7050  ledivmulOLD 7052  lemuldiv2OLD 7060  ltrec 7067  lerec 7068  lt2msq 7069  lediv12a 7079  le2msq 7086  ledivp1 7088  ledivp1i 7089  ltdivp1i 7090  lt1nnn 7130  nnleltp1 7138  nndivtr 7144  addltmul 7229  rpmulcl 7248  rpneg 7252  lble 7256  sup2 7260  suprub 7265  suprlub 7266  suprnub 7267  suprleub 7268  infmrcl 7278  xrsupsslem 7285  xrinfmsslem 7286  xrub 7289  supxr 7290  supxrre 7292  supxrunb1 7298  supxrunb2 7299  supxrbnd 7300  supxrub 7307  supxrleub 7308  dfn2 7321  lt0nnn0 7325  nnnn0addcl 7334  elnnz 7354  elnnz1 7364  nn0sub 7370  zaddcl 7374  zmulcl 7389  zltp1le 7390  btwnnz 7404  zneo 7412  uzind2 7418  uzindOLD 7420  nn0ind-raph 7426  zindd 7427  zbtwnre 7434  qaddcl 7449  qmulcl 7451  qreccl 7453  qbtwnre 7459  qsqueeze 7461  monoord 7523  iooss1 7540  iooss2 7541  elioo4g 7553  iccsupr 7567  icoshft 7577  icounlem 7581  icoun 7582  ioojoin 7585  eluz 7595  uz11 7601  eluzp1m1 7602  uzwo 7624  uzwoOLD 7625  elfzel2g 7650  fzen 7664  elfz2nn0 7667  elfz3nn0 7669  fznn0sub 7670  fsequb 7702  fsequb2 7703  fseqsupcl 7704  fseqsupubi 7705  seq1rn2 7734  ser1add2i 7751  ser1addi 7752  seqzfveq 7797  seqzrn2 7799  expp1 7817  expordi 7845  expcan 7846  expord 7847  expword2i 7850  exple1 7852  expubnd 7853  sq11 7874  sq01 7897  expnbnd 7901  expnlbnd 7902  expnlbnd2 7903  sqr0 7922  sqrlem12 7934  sqrcl 7960  sqrgt0 7961  sqrge0 7962  sqrle 7963  sqr00 7964  sqrsq 7972  sqsqr 7973  crulem 7986  replim 8011  absrpcl 8106  absid 8113  absnid 8114  leabs 8115  abssubne0 8134  absmax 8149  seq1bndi 8162  cau2i 8165  caubndi 8178  faclbnd 8197  faclbnd4lem4 8203  bccl2 8223  climcl 8238  sumeq2 8245  fsum1s 8269  fsum1s2 8270  fsump1s 8273  fsumcllem 8274  fsum1ps 8278  fsumsplit 8280  fsumadd 8282  fsumcom 8288  fsumrev 8289  fsumshftm 8292  fsummulc1 8293  fsummulc2 8294  fsumconst 8298  fsumcmp 8300  fsumcmpndx2 8302  fsumabs 8303  clm3i 8339  clm4lei 8341  clm0i 8343  clm0nnsi 8345  clmi2a 8351  climconsti 8354  climunii 8358  2climnn 8362  2climnn0 8363  climshfti 8364  iserzshft2i 8367  climge0 8372  climabs0i 8373  climaddc1 8378  climaddc2 8379  climmullem4 8383  climmullem5 8384  climmulc2 8389  climsubc2 8391  clim2serz 8394  climcmplem 8397  climserzlei 8407  climcaui 8416  caucvglem2 8418  caucvglem6 8422  caucvgi 8423  serzf0i 8429  ser1cmp2i 8437  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  cvgcmp3ce 8451  isumclim2f 8459  isumcl 8470  iserzgt0 8472  isumcmpii 8476  reccnv 8479  infcvglem3 8484  expcnv 8494  georeclim 8502  geoisumr 8505  cvgratlem2ALT 8510  cvgratlem3ALT 8511  cvgratlem1 8512  cvgratlem2 8513  cvgratlem3 8514  cvgratlem5 8516  fsum0diaglem2 8519  fsum0diag3 8522  fsum0diag4 8523  elcncf 8527  elcncf1di 8532  ivthlem9 8551  efaddlem23 8622  eftlex 8640  reeff1o 8691  efieq1re 8751  xpnnen 8768  znnen 8771  unbenlem 8773  infxpidmlem7 8827  infxpidmlem10 8830  infxpidmlem11 8831  alephexp1 8853  uniopn 8867  fiinbas 8885  tgcl 8894  tgss2 8907  basgen2 8909  subbas2 8915  subtop 8916  fctop 8920  cctop 8922  retopbas 8925  ntrval 8952  iincld 8955  clsval2 8961  0ntr 8978  elcls 8980  elcls3 8987  neii1 8997  neii2 8998  0nnei 9002  islp2 9023  clslp 9024  qdensere 9027  cnpnei 9043  cnima 9044  cnclima 9048  cnsscnp 9049  cncnplem4 9054  metxplem3 9105  metxplem4 9110  metxp 9111  rnblssm 9128  blss 9130  ssbl 9132  opnuni 9145  opnin 9146  rnblopn 9151  metequiv 9158  metcnp 9165  metcn 9167  metcnpi3 9170  metcnpi4 9171  metcni2 9173  metdnsconst 9179  cncfmet 9183  lmnn 9213  caun0 9223  lmsslem 9230  caussi 9232  metelcls 9243  metcnp4 9248  metcn4i 9250  xplmi 9251  iscms2lem3 9269  iscms2lem4 9270  iscms2lem5 9271  lmcau 9274  cmsss 9275  bcthlem2 9278  bcthlem10 9286  bcthlem21 9297  bcthlem25 9301  bcthlem28 9304  bcth 9310  grpass 9327  grpidinvlem3 9330  grpidinvlem4 9331  grpid 9349  grpasscan1 9361  grpnnncan2 9378  gxnval 9383  gxnn0suc 9387  gxid 9396  gxadd 9398  gxmul 9401  grplactf1o 9406  subgabl 9432  ghgrpilem2 9442  gapmlem 9461  gapm 9462  nvz 9629  nvcni 9661  nvcni2 9662  nvcni3 9663  nvlmle 9665  vacnlem3 9669  vacnlem4 9670  sspmval 9731  sspival 9736  sspimsval 9738  nmoub3i 9775  nmobndseqi 9780  nmlno0lem 9793  nmlnoubi 9796  lnon0 9798  nmblolbi 9800  isblo3i 9801  blocni 9805  ipasslem1 9831  ipasslem5 9835  ipdir 9843  ipass 9846  ipsubdir 9849  sspph 9856  ubthlem5 9876  ubthlem14 9887  ubthi 9889  htthlem7 9973  psref 9992  spwmo 9999  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  sineq0re 10067  efifolem2 10077  shftefif1olem 10095  eff1i 10098  twpar2 10149  dif1en 10172  indexfi 10174  fipreima 10175  dif1card 10177  findcard 10178  findcardOLD 10179  fixp 10180  cdrci 10182  hausnei2 10222  tx1cn 10223  tx2cn 10224  uptx 10226  txcnopab 10228  hmeomap 10236  hmeocna 10237  hmeocnb 10238  hmeobc 10239  cnvhmpha 10240  subtopmetlem 10255  subtopmet 10256  fipfil2 10272  fbssint 10279  infi 10280  fsubbas 10281  fbfgss 10288  fgfil 10290  filrn 10293  hausfillim 10303  elfilmap 10312  elfilmap2 10313  flimopn 10321  cncomp 10331  usinuniop 10341  lpni 10347  dirtr 10356  tosdir 10358  exidu1 10373  ismnd1 10391  unmnd 10405  fora2 10407  ringidmlem 10409  on1el4 10413  normpyc 10646  shel 10713  shsubclOLD 10723  chel 10733  hlimcauii 10739  ocorth 10797  shorth 10801  ocnel 10803  occli 10814  projlem13 10831  projlem15 10833  projlem26 10844  projlem27 10845  projlem28 10846  pjthlem13 10864  pjtheu 10869  pjpj0i 10888  pjoml 10902  shscli 10914  shsel1 10918  chintcli 10928  shlej1 10988  shmodsi 10995  shmodi 10996  h1dn0 11108  spansni 11113  spansnmul 11120  spansnss 11127  elspansn4 11129  h1datomi 11137  cm2j 11196  osumlem4 11216  osumlem6 11218  spansncvi 11232  pjige0 11271  pjsumi 11290  pjdsi 11292  pjds3i 11293  homco1 11364  homulass 11365  eigre 11398  eigorth 11401  nmopub2tALT 11470  nmfnleub2 11487  elnlfn2 11490  kbpj 11517  homco2 11538  nmlnop0iALT 11557  nmopun 11576  nmbdoplb 11587  nmcopexlem1 11588  nmcopexlem6 11593  nmcoplb 11597  nmcfnexlem1 11617  nmcfnexlem6 11622  nmcfnlb 11626  nlelchi 11631  branmfn 11675  branmfnOLD 11676  bra11 11679  cnvbraval 11681  leopadd 11703  leopmuli 11704  leopmul2i 11706  leoptr 11708  pjnmopi 11719  pjclem4 11772  pj3si 11780  hst1h 11799  stlei 11812  stlesi 11813  staddi 11818  stadd3i 11820  strlem3a 11824  hstrlem3a 11832  stcltrlem1 11848  spansncv2 11865  mdslmd1lem3 11899  mdslmd1lem4 11900  csmdsymi 11906  mdexchi 11907  atss 11918  atsseq 11919  superpos 11926  chcv1 11927  chjatom 11929  hatomic 11932  cvbr3i 11939  atcv1 11952  atexch 11953  atomli 11954  atoml2i 11955  atcvatlem 11957  atcvati 11958  atcvat2i 11959  irredlem3 11964  irredlem4 11965  atcvat3i 11968  atcvat4i 11969  mdsymlem3 11977  sumdmdii 11987  dmdbr5ati 11994  cdj1i 12005  cdj3lem1 12006  cdj3lem2b 12009  bnj2 12367  bnj9 12372  bnj9OLD 12373  bnj10 12374  bnj44 12419  bnj44OLD 12420  bnj48 12422  bnj48OLD 12423  bnj55 12430  bnj148 12481  bnj162OLD 12488  bnj559 12539  bnj588 12554  bnj599OLD 12561  bnj945 12844  bnj1115 12926  bnj1215 12991  bnj1337 13064  bnj547 13273  bnj594 13300  bnj1017 13377  bnj1118 13420  bnj1280 13483  fndmeng 13598  fz1eqblem 13608  fseq1cl 13619  ghomgsg 13636  ghomf1olem 13637  negn0 13655  lbzbi 13657  dvds0lem 13665  dvdscmulr 13682  dvdsmulcr 13683  dvds2ln 13684  dvdsle 13693  divalglem5 13700  divalglem8 13703  divalgb 13707  ndvdsadd 13711  gcdcllem1 13718  dvdslegcd 13723  gcd0id 13729  gcdneg 13732  algfx 13748  eucalgcvga 13754  1nprm 13769  zgt1b1 13771  isprm2lem 13774  isprm3 13776  fundmpss 13836  dfon2lem3 13851  dfon2lem5 13853  dfon2lem6 13854  dfon2lem8 13856  dfon2lem9 13857  axext4dist 13867  setlikess 13906  preddowncl 13907  wfi 13915  frmin 13938  frind 13939  poxp 13949  soxp 13950  poseq 13954  soseq 13955  wfrlem4 13960  wfrlem10 13966  wfrlem12 13968  nofv 13998  noreson 14001  axsltsolem1 14006  axdenselem3 14021  axdenselem4 14022  axdenselem5 14023  axdenselem7 14025  axdenselem8 14026  axdense 14027  nocvxminlem 14028  nocvxmin 14029  axfelem5 14035  axfelem7 14037  axfelem8 14038  axfelem9 14039  axfelem12 14042  axfelem14 14044  axfelem15 14045  axfelem16 14046  findabrcl 14255  ee7.2aOLD 14262  nxtand 14313  fnoprvpop 14338  uninqs 14340  infi1 14343  ficli 14353  f2imacnv 14355  oooeqim2 14356  domrngref 14364  imgfldref2 14368  ref4w 14370  f1fi 14377  cpref 14379  inttr 14384  njtlc 14389  surrc2 14390  restidsing 14391  twsymr 14394  prj1 14395  imfstnrelc 14396  unpde2eg22 14407  imrestr 14426  sndw 14428  inttrp 14437  reflincror 14446  cnveq2 14455  injrec 14461  surjsec 14462  injrec2 14466  surjsec2 14467  inpreima2 14468  inpreima5 14469  fopab2g 14485  npincppr 14501  repcpwti 14503  cbcpcp 14504  prjmapcp 14507  cbicplem 14508  unprj 14511  prl 14512  prl2 14514  jidd 14540  midd 14541  cur1vald 14547  domrancur1b 14548  domrancur1c 14550  preoref22 14570  preotr2 14576  int2pre 14578  ubos2 14598  defse3 14614  suplub2 14616  inposet 14620  istoset2 14628  pospos 14635  tostos 14637  toplat 14638  latdir 14643  prodeq2 14661  fprod1s 14677  fprod1s2 14678  fprodp1s 14682  ridlideq 14695  rzrlzreq 14696  reacomsmgrp2 14704  clfsebs 14707  fincmpzer 14711  resgcom 14712  fprodadd 14713  gaplc 14731  fnopabco2b 14734  curgrpact 14735  grpdivone 14736  grpdlcan 14739  fprodsub 14742  trran2 14757  prsubrtr 14763  rnginvcl 14770  fldi 14776  rngridfz 14786  claddinvvec 14803  vec2inv 14804  addnull2 14807  addvecass 14808  addvecom 14809  invaddvec 14810  vecsrcan 14812  vecslcan 14813  vecrcan 14818  veclcan 14819  muldisc 14824  svli2 14826  svs2 14829  svs3 14830  truni1 14849  truni3 14851  cexint2 14862  intfmu2 14867  cmphmp 14878  cnvhmphb 14880  hmphre 14884  hmphtr 14885  hmeogrp 14892  homcard 14893  top2ind 14897  homindlem2 14899  intcont 14914  prtoptop 14919  fgsb 14921  efilcp 14922  fgsb2 14925  efilcp2 14926  cnfilca 14927  rcfpfillem4 14931  limfillem2 14939  limfilnei 14943  conttnf 14944  iscnp3 14946  cnpfillim4 14947  stfincomp 14959  bwt2 14960  topsinind 14967  trhom 14983  tpgprop2 14987  altretop 14997  cntrsetlem 14999  iintlem1 15010  trnij 15015  xrletr2 15018  lvsovso 15038  lvsovso3 15040  supnuf 15041  idosd 15091  rdmob 15095  cmpasso 15120  dualalg 15131  dualcat2 15133  cmpassoh 15150  homgrf 15151  imonclem 15162  ismonc 15163  cmpmon 15164  icmpmon 15165  idmon 15166  iepiclem 15172  isepic 15173  fmp 15188  obsubc2 15198  idsubc 15199  domsubc 15200  codsubc 15201  cmpsubc 15204  taralt 15211  tarax3a 15222  tarax3d2 15225  tarax3e 15228  tarcrpr 15237  elcartr 15238  cptarc 15242  bpmp 15251  btmp 15252  intartar 15255  tartarmap 15265  pwtsm 15266  subtsm 15267  vtarsuelt 15272  partarelt2 15274  inttaror 15277  carinttar 15279  elcarelcl 15283  fnctartar 15284  fnctartar2 15285  isline1 15294  isseg1 15304  imp5g 15332  imp5q 15349  eqeu 15351  finminlem 15367  ordisoOLD 15374  ordtypelem4OLD 15378  ordtypelem6OLD 15380  ordtypelem7OLD 15381  ordtypeOLD 15382  hartogOLD 15384  omsubsuc2OLD 15387  omsubsdomlem2OLD 15389  omsubsdomOLD 15390  omsubelOLD 15392  omsubindssOLD 15397  infenomsubOLD 15398  clsint2 15414  opnnei 15417  cncls 15419  cnsubsp 15426  cnsubsp2 15427  compsublem 15430  compsub 15431  cptclsscpt 15432  uncomp 15433  hscptsscld 15434  compfipin0lem 15435  alexsublem2 15438  alexsublem4 15440  alexsub 15441  dfcon2 15442  connsub 15443  cnconn 15444  reconnlem1 15446  reconnlem5 15450  iccconn 15453  ivthALT 15454  topfneec 15501  ptfinfin 15508  lfinpfin 15513  locfincomp 15514  comppfsc 15517  neibastop3 15524  topmtcl 15525  topjoin 15527  fnejoin1 15530  fnejoin2 15531  t0dist 15541  ist1-3 15543  t1sncld 15545  t1sep 15546  regsep 15550  nrmsep 15554  nrmsep2 15555  supfil 15560  filfinnfr 15561  isufil2 15565  ufilss 15567  ufprim 15569  filssufillem 15570  filssufil 15571  ufileulem 15572  ufileu 15573  uffixfr 15575  ufilen 15579  limfilcf 15587  flimcls 15588  cnpfillim 15589  rnelfm 15593  fmfnfmlem1 15594  fmfnfmlem4 15597  fmfnfm 15598  flimfbas 15601  fclusneii 15609  fclusbas 15610  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  fcluscnp 15618  isfclusf 15625  tailfb 15639  filnetlem5 15644  unirep 15664  cover2 15673  foco2 15686  cocanfo 15689  xpeng 15691  enf1f1o 15720  ecelqsg 15731  eropreu 15733  fimax 15746  ac6gf 15749  indexa 15753  indexdom 15754  indexfiOLD 15755  fipreimaOLD 15756  inficl 15757  supclt 15762  supubt 15763  infmrlb 15765  infmrgelb 15766  supeut 15767  frfi 15771  pofun 15772  fimaxre 15774  filbcmb 15776  add20 15777  eluzadd 15782  fzfi2 15787  fzn0 15789  fzmul 15790  fzsplit 15792  fzdisj 15793  fzm1 15796  rddif 15798  absrdbnd 15799  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  seq1eq2 15817  nnubfi 15818  nninfnub 15819  fsum00 15820  fsumlt 15821  fsumltisum 15824  fsumleisum 15827  fsumlt1 15831  metf1o 15843  blhalf 15846  mettrifi 15847  mettrifi2 15848  geomcau 15849  lmclim2 15850  metdcn 15853  iccsplit 15854  icoopnst 15876  iocopnst 15877  lincmb01icc 15879  oprpiece1res2 15881  cncfco 15887  cnres 15889  paste 15893  hmeoopn 15899  hmeocld 15900  lmtlm 15908  txcnoprab 15911  txsubsp 15912  txcld 15914  txmet 15925  sstotbnd 15936  totbndss 15937  isbnd3 15941  bndss 15942  totbndbnd 15944  ismtyhmeolem 15950  ismtybndlem 15952  ismtyres 15954  heiborlem1 15955  heiborlem11 15965  heiborlem13 15967  heiborlem15 15969  heiborlem16 15970  heiborlem23 15977  heiborlem27 15981  heiborlem29 15983  heiborlem31 15985  heiborlem32 15986  heiborlem35 15989  heiborlem36 15990  rrndstprj2 16018  rrncms 16019  rrntotbndlem1 16020  rrntotbnd 16022  reheibor 16025  iccbnd 16026  exidreslem 16030  abl4pnp 16037  ghomco 16040  phtpyval 16047  reparpht 16065  pcohtpy 16083  pcoass 16085  pcorevlem 16086  pi1gp 16095  ringsubdi 16106  ringsubdir 16107  divrngcl 16110  isdivrng2 16111  isdivrng3 16112  rnghomco 16128  rngisocnv 16135  riscer 16142  divrngidl 16176  intidl 16177  unichnidl 16179  keridl 16180  ispridl2 16186  isfldidl 16216  dmncan1 16224  impbidd 16227  bicomddOLD 16229  jca3 16233  pm5.31r 16240  erdisj3 16266  prtlem18 16279  prtlem19 16280  prter2 16285  prter3 16286  pm10.56 16317  pm13.14 16370  pm13.18OLD 16371  xrltneNEW 16434  xpexcnv 16436  smoge 16454  e222 16526  fnelstr 16717  pltnle 16786  joinlem 16817  meetlem 16824  clatlem 16889  clatlat 16893  lubun 16899  lubunNEW 16900  clatleglb 16903  omllaw3 16966  cmtbr3 16975  glbconx 17029  hlexchb 17035  hlsupr 17036  hlrelat5 17050  hlrelat 17051  hl2atom 17053  cvr1 17054  cvrexchlem 17059  cvratlem 17061  cvrat 17062  cvrat2 17066  cvrat3 17075  cvrat4 17076  ps-1 17078  ps2 17079  grpidinvlem3NEW 17111  grpidinvlem4NEW 17112  grpidNEW 17124  pointpsub 17231  linepsub 17232  pmapglbx 17251  pmapglb2x 17254  elpaddn0 17261  paddss12 17280  paddasslem1 17281  paddasslem15 17295  paddasslem16 17296  pmodlem1 17307  pmodlem2 17308  pmodi 17309  pmapjat 17314  linepsubcl 17359  poml6 17363  pexmidOLD 17386

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain