MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expcom Unicode version

Theorem expcom 435
Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
ex.1
Assertion
Ref Expression
expcom

Proof of Theorem expcom
StepHypRef Expression
1 ex.1 . . 3
21ex 434 . 2
32com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  ancoms  453  syldan  470  sylan  471  4casesdan  950  dedlema  954  dedlemb  955  19.40b  1698  cbval2  2027  cbvex2OLD  2029  2moswap  2369  2eu2  2378  pm2.61ne  2772  pm2.61neOLD  2773  r19.21be  2828  uneqdifeq  3916  raltpd  4153  ssunsn2  4189  ssuni  4271  uniss2  4282  elpwuni  4418  elssabg  4607  elpw2g  4615  oteqex  4745  epelg  4797  wereu  4880  ordtr2  4927  ordsssuc2  4971  relop  5158  riinint  5264  sotri3  5402  unixpid  5547  cnviin  5549  funopg  5625  fun  5753  tz6.12c  5890  fvmptnf  5973  fvn0ssdmfun  6022  eldmrexrnb  6038  fmptco  6064  fnressn  6083  fressnfv  6085  fvtp2g  6122  fvtp3g  6123  fconst2g  6125  f1dom3el3dif  6176  isores3  6231  isoselem  6237  oprabv  6345  eloprabga  6389  sorpsscmpl  6591  difex2  6607  ordpwsuc  6650  ordsucun  6660  limuni3  6687  ordom  6709  fo1stres  6824  poxp  6912  soxp  6913  suppimacnv  6929  frnsuppeq  6930  funsssuppss  6945  brtpos2  6980  onnseq  7034  smores  7042  smofvon2  7046  tfrlem1  7064  oacl  7204  omcl  7205  oecl  7206  oawordri  7218  oalimcl  7228  oaass  7229  oarec  7230  omwordri  7240  omeulem1  7250  omeulem2  7251  oeordi  7255  oeworde  7261  oeoelem  7266  nnacl  7279  nnmcl  7280  nnecl  7281  nnacom  7285  nnaass  7290  nnmsucr  7293  nnmordi  7299  omabs  7315  iiner  7402  elpmg  7454  pmss12g  7465  mapsn  7480  f1domg  7555  ssdomg  7581  domtriord  7683  php  7721  php3  7723  1sdom  7742  fisseneq  7751  isinf  7753  ssnnfi  7759  dif1enOLD  7772  dif1en  7773  findcard3  7783  frfi  7785  unfi  7807  difinf  7810  fnfi  7818  iunfi  7828  fsuppunfi  7869  fsuppres  7874  frnfsuppbi  7878  elfi2  7894  marypha1lem  7913  marypha1  7914  oiexg  7981  wemapso2  8000  harword  8012  brwdom  8014  unxpwdom  8036  en3lplem1  8052  inf3lemd  8065  inf3lem5  8070  cantnfval2  8109  cantnfle  8111  cantnflt  8112  cantnfval2OLD  8139  cantnfleOLD  8141  cantnfltOLD  8142  cnfcom  8165  cnfcomOLD  8173  tcmin  8193  r1sdom  8213  rankxplim3  8320  cardidm  8361  cardmin2  8400  infxpenlem  8412  fseqenlem1  8426  numacn  8451  alephordi  8476  iscard3  8495  alephinit  8497  carduniima  8498  iunfictbso  8516  dfac5  8530  dfac12lem3  8546  pwsdompw  8605  pwcdadom  8617  cflim2  8664  cfslb2n  8669  cofsmo  8670  cfsmolem  8671  cfcoflem  8673  alephsing  8677  infpssALT  8714  fin23lem34  8747  isf32lem2  8755  isf32lem10  8763  isf32lem12  8765  isfin1-2  8786  hsmexlem4  8830  axcc2lem  8837  domtriomlem  8843  axdc2lem  8849  axdc3lem2  8852  axdc3lem4  8854  axdc4lem  8856  axcclem  8858  ac6num  8880  ac6s  8885  zorn2lem7  8903  ttukeylem5  8914  imadomg  8933  iundom2g  8936  ondomon  8959  ficard  8961  konigthlem  8964  alephreg  8978  pwcfsdom  8979  cfpwsdom  8980  axregndlem1  9000  axregnd  9002  axregndOLD  9003  pwfseqlem3  9059  pwxpndom2  9064  pwxpndom  9065  pwcdandom  9066  inawinalem  9088  gchina  9098  wuncval2  9146  tsk0  9162  tskxpss  9171  inatsk  9177  tskuni  9182  gruina  9217  grothac  9229  addclpi  9291  addnidpi  9300  nqereu  9328  mulcanenq  9359  genpnnp  9404  nqpr  9413  prlem934  9432  reclem2pr  9447  suplem1pr  9451  supsrlem  9509  axpre-sup  9567  1re  9616  dedekindle  9766  00id  9776  receu  10219  sup3  10525  peano5nni  10564  nnaddcl  10583  zrevaddcl  10934  zdiv  10958  nneo  10971  zeo2  10974  nn0indd  10986  fzind  10987  fnn0ind  10988  uzwo  11173  uzwoOLD  11174  lbzbi  11199  nn01to3  11204  qrevaddcl  11233  irradd  11235  irrmul  11236  ltsubrp  11280  ltaddrp  11281  icoshft  11671  fzen  11732  elfzm11  11778  uzsplit  11779  elfzom1elp1fzo  11883  injresinjlem  11925  injresinj  11926  modifeq2int  12049  om2uzlti  12061  ssnn0fi  12094  fsuppmapnn0fiub0  12099  mptnn0fsuppr  12105  seqcl2  12125  seqfveq2  12129  seqshft2  12133  monoord  12137  seqsplit  12140  seqcaopr3  12142  seqf1olem2a  12145  seqf1o  12148  seqid2  12153  seqhomo  12154  ser1const  12163  expadd  12208  expmul  12211  leexp1a  12224  faccl  12363  facdiv  12365  faclbnd  12368  faclbnd4lem4  12374  faclbnd6  12377  hasheqf1oi  12424  hashf1rn  12425  hashgadd  12445  hashinfxadd  12453  hashunx  12454  hashunsng  12459  elprchashprn2  12461  hashle00  12465  hashss  12474  hash1snb  12479  hashmap  12493  hashf1lem2  12505  hashf1  12506  seqcoll  12512  hashge2el2dif  12521  hashge3el3dif  12524  hash1to3  12530  brfi1uzind  12532  sswrd  12555  swrdvalodm2  12664  swrdvalodm  12665  swrdswrdlem  12684  swrdswrd  12685  wrd2ind  12703  swrdccatin1  12708  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccat3  12717  repsdf2  12750  repswswrd  12756  cshw0  12765  cshwcl  12769  cshwlen  12770  swrdco  12803  shftlem  12901  caubnd  13191  rlimcld2  13401  o1dif  13452  climub  13484  climserle  13485  iseraltlem2  13505  sumss  13546  fsumzcl2  13560  fsummsnunz  13569  fsumsplitsnun  13570  fsum2d  13586  modfsummods  13607  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  bcxmas  13647  climcndslem1  13661  climcndslem2  13662  cvgrat  13692  clim2prod  13697  prodfn0  13703  prodfrec  13704  ntrivcvg  13706  prodmo  13743  fprodss  13755  fprodabs  13778  fprodn0  13783  fprod2d  13785  fprodefsum  13830  sin01gt0  13925  ruclem8  13970  ruclem9  13971  dvds2ln  14014  dvdslelem  14030  alzdvds  14036  ndvdsadd  14066  bitsinv1  14092  sadcadd  14108  sadadd2  14110  saddisjlem  14114  smuval2  14132  smupvallem  14133  smu01lem  14135  smupval  14138  smueqlem  14140  smumullem  14142  gcddiv  14187  gcdmultiple  14188  rplpwr  14194  nn0seqcvgd  14199  seq1st  14200  alginv  14204  algcvga  14208  algfx  14209  isprm2  14225  isprm3  14226  prmind2  14228  maxprmfct  14254  prmdvdsexp  14255  pcmpt  14411  prmreclem4  14437  vdwmc2  14497  vdwlem10  14508  ramub2  14532  ramcl  14547  cshwshashlem1  14580  cshwshashlem3  14582  imasleval  14938  divsfval  14944  mreexexlem4d  15044  isssc  15189  istos  15665  mgmcl  15875  mndclOLD  15931  mndassOLD  15932  frmdgsum  16030  mhmmulg  16174  resghm2b  16285  gsumwrev  16401  elsymgbas  16407  symgextf1  16446  gsmsymgreqlem2  16456  gsmsymgreq  16457  odlem1  16559  odcl2  16587  gexlem1  16599  sylow1lem1  16618  efgi2  16743  efginvrel2  16745  efgsrel  16752  cyggexb  16901  gsummulglem  16964  gsumzunsnd  16982  gsum2dlem2  16998  gsum2dOLD  17000  telgsums  17022  dmdprd  17029  dprdw  17043  dprdwOLD  17050  ablfac1eulem  17123  srgpcomp  17183  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  cply1mul  18335  coe1fzgsumdlem  18343  gsummoncoe1  18346  pf1ind  18391  evl1gsumdlem  18392  cnfldmulg  18450  cnfldexp  18451  obslbs  18761  mat1dimcrng  18979  ma1repveval  19073  mulmarep1gsum2  19076  gsummatr01lem3  19159  cramerlem3  19191  decpmatmulsumfsupp  19274  mp2pm2mplem4  19310  pm2mpmhmlem1  19319  fvmptnn04if  19350  cayhamlem1  19367  fctop  19505  mretopd  19593  restopnb  19676  restdis  19679  tgcnp  19754  cncls2  19774  cncls  19775  cnntr  19776  cnsscnp  19780  cmpsub  19900  2ndcsep  19960  1stcelcls  19962  lfinpfin  20025  locfincmp  20027  comppfsc  20033  txcn  20127  txlm  20149  xkohaus  20154  qtopres  20199  haushmphlem  20288  cmphmph  20289  conhmph  20290  reghmph  20294  nrmhmph  20295  ptcmpfi  20314  reghaus  20326  fbssfi  20338  fbun  20341  fbfinnfr  20342  isfildlem  20358  fgcl  20379  cfinfil  20394  supfil  20396  ufinffr  20430  fin1aufil  20433  cnpflf  20502  alexsubALTlem3  20549  alexsubALT  20551  cnextfvval  20565  cnextcn  20567  tmdmulg  20591  tmdgsum  20594  tgphaus  20615  tgpt1  20616  mettri  20855  imasdsf1olem  20876  blssexps  20929  blssex  20930  mopni3  20997  metss  21011  metutopOLD  21085  psmetutop  21086  dscmet  21093  rectbntr0  21337  metnrmlem1a  21362  fsumcn  21374  lmmbr  21697  caubl  21746  caublcls  21747  bcthlem5  21767  bcth3  21770  ovolunlem1a  21907  ovoliunnul  21918  ovolicc2lem3  21930  finiunmbl  21954  voliunlem1  21960  volsuplem  21965  volsup  21966  dyadmax  22007  itgfsum  22233  dvnadd  22332  dvnres  22334  cpnord  22338  dvnfre  22355  dvmptfsum  22376  dvlip  22394  fta1g  22568  plyco  22638  dgrcolem1  22670  dgrco  22672  dvnply2  22683  plydivex  22693  plyexmo  22709  aannenlem1  22724  aaliou3lem2  22739  dvntaylp  22766  taylthlem1  22768  ulmval  22775  cxpmul2  23070  scvxcvx  23315  jensenlem2  23317  jensen  23318  ppiub  23479  bcmono  23552  bpos1lem  23557  bposlem5  23563  lgsquad2lem2  23634  dchrisumlem1  23674  dchrisum0flb  23695  pntpbnd1  23771  pntlemf  23790  qabvle  23810  qabvexp  23811  ostthlem2  23813  ostth2lem2  23819  axeuclidlem  24265  axcontlem12  24278  usgraedgprv  24376  usgranloopv  24378  usgraidx2vlem2  24392  usgrafisbase  24414  edgusgranbfin  24450  nb3graprlem2  24452  cusgra2v  24462  cusgrafi  24482  sizeusglecusglem1  24484  sizeusglecusg  24486  usgramaxsize  24487  iswlkg  24524  2trllemH  24554  2trllemE  24555  usgrnloop  24565  spthonepeq  24589  wlkdvspthlem  24609  wlkdvspth  24610  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  cyclnspth  24631  fargshiftf  24636  fargshiftf1  24637  3v3e3cycl2  24664  3v3e3cycl  24665  4cycl4dv  24667  wwlkn0  24689  usg2wlkeq  24708  wwlknred  24723  wwlkextfun  24729  wwlkextinj  24730  wwlkm1edg  24735  wwlkextproplem3  24743  clwwlkgt0  24771  clwlkisclwwlklem1  24787  clwlkisclwwlklem0  24788  wwlksubclwwlk  24804  clwwisshclww  24807  clwwisshclwwn  24808  clwlkfclwwlk  24844  2wlkonot3v  24875  2spthonot3v  24876  usg2wlkonot  24883  usg2wotspth  24884  usgfidegfi  24910  cusgraisrusgra  24938  rusgranumwlk  24957  iseupa  24965  eupatrl  24968  eupath2  24980  frgra2v  24999  frgra3vlem1  25000  3vfriswmgra  25005  1to2vfriswmgra  25006  1to3vfriswmgra  25007  2pthfrgra  25011  3cyclfrgrarn1  25012  3cyclfrgrarn  25013  3cyclfrgrarn2  25014  4cycl2vnunb  25017  vdn0frgrav2  25023  vdgn0frgrav2  25024  frgrancvvdeqlem4  25033  frgrancvvdeqlemB  25038  frgrancvvdeqlemC  25039  frgrawopreglem2  25045  frgrawopreglem4  25047  frgrawopreg  25049  frgraregorufr0  25052  frgraeu  25054  frg2woteqm  25059  2spotmdisj  25068  usgreghash2spot  25069  clwwlkextfrlem1  25076  numclwwlkovf2ex  25086  numclwlk1lem2foa  25091  numclwlk1lem2f1  25094  frgrareg  25117  friendshipgt3  25121  elghomlem2OLD  25364  isrngo  25380  rngodm1dm2  25420  rngoridfz  25437  hlim2  26109  elnlfn  26847  stle0i  27158  hstrbi  27185  spansncv2  27212  h1da  27268  fmptcof2  27502  xreceu  27618  tpr2rico  27894  hasheuni  28091  ismeas  28170  sseqp1  28334  rrvsum  28393  dstfrvunirn  28413  sgn3da  28480  subfacp1lem6  28629  cvmliftlem7  28736  cvmliftlem10  28739  cvmlift2lem12  28759  cvmlift3lem4  28767  mrsubvrs  28882  ghomf1olem  29034  climuzcnv  29037  relexpsucr  29053  relexpsucl  29055  relexpcnv  29056  relexprel  29057  relexpdm  29058  relexprn  29059  relexpfld  29060  relexpadd  29061  relexpindlem  29062  rtrclreclem.trans  29069  rtrclreclem.min  29070  rtrclind  29072  iprodefisumlem  29123  fprb  29203  dfon2lem9  29223  trpredtr  29313  trpredmintr  29314  dftrpred3g  29316  trpredrec  29321  soseq  29334  wfrlem12  29354  frrlem11  29399  sltval2  29416  sltsolem1  29428  linethru  29803  elhf2  29832  nndivsub  29922  wl-exeq  29987  wl-ax11-lem3  30027  heicant  30049  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  finminlem  30136  fnessref  30175  neibastop2lem  30178  fnemeet2  30185  cover2  30204  upixp  30220  sdclem2  30235  fdc  30238  seqpo  30240  metf1o  30248  mettrifi  30250  sstotbnd3  30272  heibor1lem  30305  heiborlem5  30311  heibor  30317  bfplem1  30318  grpokerinj  30347  ispridl2  30435  exlimddvf  30526  mzpsubst  30681  jm2.18  30930  wepwsolem  30987  dvgrat  31193  radcnvrat  31195  islptre  31625  iblspltprt  31772  stoweidlem2  31784  stoweidlem17  31799  stoweidlem21  31803  2reu2  32192  afveu  32238  funbrafv  32243  ndmaovass  32291  2elfz2melfz  32334  fzoopth  32340  fsummsndifre  32345  fsumsplitsndif  32346  fsummmodsndifre  32347  fsummmodsnunz  32348  usgedgvadf1lem2  32414  usgedgvadf1ALTlem2  32417  clcllaw  32515  initoeu1  32617  termoeu1  32624  nrhmzr  32679  rnghmmul  32706  rngccatidOLD  32797  ringccatidOLD  32860  nzerooringczr  32880  scmsuppss  32965  gsumlsscl  32976  ply1mulgsumlem2  32987  lincvalsc0  33022  linc0scn0  33024  lincdifsn  33025  linc1  33026  lincellss  33027  lincsum  33030  lincscm  33031  lincsumcl  33032  lcoss  33037  lincext3  33057  lindslinindimp2lem4  33062  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  lindsrng01  33069  snlindsntor  33072  lincresunit3lem2  33081  lincresunit3  33082  islindeps2  33084  sbcoreleleqVD  33659  csbxpgVD  33694  sineq0ALT  33737  bnj607  33974  bnj1145  34049  bnj1204  34068  bj-cbval2v  34302  bj-xpnzex  34516  lssatle  34740  4atexlemex4  35797
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 185  df-an 371
  Copyright terms: Public domain W3C validator