Theorem impcom 430

Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
imp.1

Assertion

Ref	Expression
impcom

Proof of Theorem impcom

Step	Hyp	Ref	Expression
1		imp.1	. . 3
2	1	com12 31	. 2
3	2	imp 429	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  mpan9  469  ornldOLD  899  bianir  967  19.41v  1771  equtr2  1802  19.41  1971  nfsb4t  2130  ax12eq  2271  ax12el  2272  mopickOLD  2357  2euex  2366  gencl  3139  2gencl  3140  vtocl4g  3178  rspccva  3209  sbcimdvOLD  3397  sseq0  3817  minel  3882  r19.2z  3918  elelpwi  4023  ssuni  4271  disji2  4439  disjiun  4442  trint0  4562  ssexg  4598  pofun  4821  solin  4828  2optocl  5082  3optocl  5083  elrnmpt1  5256  resieq  5289  funimaexg  5670  fnun  5692  fss  5744  fun  5753  fvelimab  5929  fvmptss  5964  fvn0ssdmfun  6022  fvcofneq  6039  fmptco  6064  fnressn  6083  fressnfv  6085  fvn0fvelrn  6088  fmptsng  6092  fvtp2g  6122  fvtp3g  6123  fnex  6139  funfvima3  6149  isores3  6231  dmfex  6758  f1o2ndf1  6908  frxp  6910  fnse  6917  ressuppssdif  6940  funsssuppss  6945  suppss  6949  mpt2xopxnop0  6962  reldmtpos  6982  smores  7042  tfrlem7  7071  tz7.48-2  7126  tz7.49  7129  oacl  7204  omcl  7205  oecl  7206  oarec  7230  oewordri  7260  oeworde  7261  oelim2  7263  oeoa  7265  oeoelem  7266  oeoe  7267  nnacl  7279  nnmcl  7280  nnecl  7281  nnmsucr  7293  2ecoptocl  7421  undifixp  7525  xpf1o  7699  limensuc  7714  ac6sfi  7784  frfi  7785  difinf  7810  suppeqfsuppbi  7863  elfiun  7910  dffi3  7911  xpwdomg  8032  preleq  8055  infdiffi  8095  epfrs  8183  rankxpsuc  8321  tskwe  8352  infxpenlem  8412  fseqenlem1  8426  kmlem2  8552  cff1  8659  cflim2  8664  sornom  8678  infpssrlem4  8707  fin23lem26  8726  fin23lem30  8743  fin23lem34  8747  isf32lem11  8764  fin67  8796  isfin7-2  8797  fin1a2lem10  8810  axcc2lem  8837  axdc2lem  8849  axdc3lem2  8852  axdc3lem4  8854  axdc4lem  8856  iunfo  8935  tsk0  9162  gruina  9217  grur1a  9218  mulcanenq  9359  reclem2pr  9447  supsrlem  9509  supsr  9510  ax1rid  9559  mulgt1  10426  lbreu  10518  nnaddcl  10583  nnmulcl  10584  nn0n0n1ge2b  10885  nn0indd  10986  fzind  10987  fnn0ind  10988  uzaddcl  11166  nn01to3  11204  xmulasslem2  11503  supxrunb1  11540  supxrunb2  11541  uzsubsubfz  11736  elfz1b  11777  elfz0ubfz0  11807  fz0fzdiffz0  11812  elfzmlbmOLD  11814  elfzmlbp  11815  fzofzim  11869  elfzom1elp1fzo  11883  elfzom1p1elfzo  11895  ssfzo12bi  11907  fzonfzoufzol  11913  elfznelfzob  11916  injresinjlem  11925  injresinj  11926  modaddmodup  12050  om2uzlti  12061  fsequb  12085  ssnn0fi  12094  ser1const  12163  expcllem  12177  expeq0  12196  faclbnd  12368  faclbnd6  12377  hasheqf1oi  12424  hashf1rn  12425  hashgadd  12445  hashunx  12454  hashnn0n0nn  12458  hashgt0elex  12466  hashss  12474  hashxp  12492  hashimarni  12497  seqcoll  12512  hash2prb  12517  hash2prv  12525  hash2sspr  12526  brfi1indlem  12531  brfi1uzind  12532  lswlgt0cl  12590  swrd0  12658  swrdvalodm2  12664  swrdspsleq  12673  2swrd1eqwrdeq  12679  disjxwrd  12680  swrdswrdlem  12684  swrdswrd  12685  wrd2ind  12703  swrdccatfn  12707  swrdccatin1  12708  swrdccatin12lem2a  12710  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccatin12lem3  12715  swrdccatin12  12716  swrdccat3  12717  swrdccat  12718  swrdccat3blem  12720  repswswrd  12756  repswrevw  12758  cshwmodn  12766  cshwsublen  12767  cshwidxmod  12774  2cshw  12781  cshweqrep  12789  cshw1  12790  2cshwcshw  12793  cshwcshid  12795  cshwcsh2id  12796  wrdlen2i  12884  2swrd2eqwrdeq  12891  wwlktovfo  12896  cjexp  12983  absexp  13137  r19.29uz  13183  caubnd  13191  sqreu  13193  climshft  13399  climub  13484  climserle  13485  sumss  13546  sumss2  13548  modfsummods  13607  o1fsum  13627  binom  13642  bcxmas  13647  climcndslem1  13661  climcndslem2  13662  cvgrat  13692  clim2prod  13697  prodfn0  13703  prodfrec  13704  ntrivcvgfvn0  13708  fprodn0  13783  fprodefsum  13830  demoivreALT  13936  znnenlem  13945  ruclem8  13970  dvdsfac  14041  smu01lem  14135  dvdslegcd  14154  gcdneg  14164  gcdmultiple  14188  seq1st  14200  alginv  14204  prmdvdsexp  14255  cshwshashlem1  14580  catsubcat  15208  lubss  15751  lubel  15752  mgmb1mgm1  15883  frmdgsum  16030  mgm2nsgrplem3  16038  gaass  16335  gsumwrev  16401  symgextf1lem  16445  symgextf1  16446  fvcosymgeq  16454  gsmsymgreq  16457  symgfixelsi  16460  pmtrprfv3  16479  symggen  16495  pmtrprfval  16512  gsumzres  16914  gsumzunsnd  16982  srgmulgass  17182  srgbinom  17196  lmodvsmmulgdi  17547  0ringnnzr  17917  assamulgscm  17999  gsumply1subr  18275  gsummoncoe1  18346  pf1ind  18391  cnfldmulg  18450  cnfldexp  18451  psgndiflemB  18636  matmulcell  18947  mat1dimscm  18977  dmatmul  18999  dmatscmcl  19005  scmataddcl  19018  scmatsubcl  19019  scmatsgrp1  19024  mavmulsolcl  19053  ma1repveval  19073  1marepvmarrepid  19077  symgmatr01lem  19155  slesolvec  19181  cramerimplem2  19186  decpmatmullem  19272  pm2mpf1  19300  mp2pm2mplem4  19310  monmat2matmon  19325  chpscmat  19343  chpscmatgsumbin  19345  fvmptnn04ifb  19352  chfacfscmul0  19359  chfacfscmulgsum  19361  chfacfpmmul0  19363  chfacfpmmulgsum  19365  cpmadugsumlemF  19377  clsss  19555  ntrss  19556  restntr  19683  cmpsublem  19899  cmpsub  19900  bwthOLD  19911  2ndcrest  19955  txindislem  20134  t0kq  20319  filufint  20421  fbflim2  20478  flftg  20497  alexsubALTlem4  20550  cnextfvval  20565  tmdmulg  20591  ustuqtop4  20747  xmettri2  20843  mettri  20855  metss  21011  lmmbr  21697  caublcls  21747  lmcau  21751  ovolunlem1a  21907  nulmbl2  21947  voliunlem1  21960  iunmbl  21963  volsup  21966  dvlip  22394  dvfsumle  22422  degltlem1  22472  ply1divex  22537  plyco  22638  dgrnznn  22644  dvnply2  22683  plydivex  22693  aannenlem2  22725  aaliou3lem2  22739  ulmcau  22790  dchrisumlem1  23674  dchrisumlem2  23675  dchrisumlem3  23676  qabvle  23810  ostthlem2  23813  ostth2lem2  23819  axeuclidlem  24265  usgra2edg  24382  usgraedg4  24387  usgraidx2vlem2  24392  nbusgra  24428  nbgraf1olem5  24445  nb3graprlem1  24451  nb3graprlem2  24452  cusgrarn  24459  nbcusgra  24463  cusgrasize2inds  24477  sizeusglecusglem1  24484  uvtxnbgra  24493  iswlkg  24524  wlkn0  24527  usgrnloop  24565  redwlk  24608  wlkdvspthlem  24609  usgra2adedgwlkonALT  24616  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  usgra2wlkspth  24621  fargshiftf1  24637  usgrcyclnl1  24640  usgrcyclnl2  24641  nvnencycllem  24643  constr3trllem2  24651  wwlknimp  24687  wlkiswwlk1  24690  wlkiswwlk2  24697  wlklniswwlkn1  24699  wlklniswwlkn2  24700  vfwlkniswwlkn  24706  wwlknext  24724  wwlknredwwlkn  24726  wwlknredwwlkn0  24727  wwlkextfun  24729  wwlkextinj  24730  wwlkextsur  24731  wwlkextproplem3  24743  clwlkisclwwlklem2a1  24779  clwlkisclwwlklem2fv2  24783  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwwlkel  24793  clwwlkf1  24796  clwwlkfo  24797  clwwlknwwlkncl  24800  clwwlkext2edg  24802  wwlkext2clwwlk  24803  wwlksubclwwlk  24804  clwwisshclwwlem  24806  clwwisshclww  24807  clwwisshclwwn  24808  erclwwlktr  24815  clwwlknscsh  24819  erclwwlkntr  24827  eleclclwwlkn  24833  hashecclwwlkn1  24834  usghashecclwwlk  24835  clwlkfclwwlk  24844  clwlkfoclwwlk  24845  el2wlkonot  24869  el2spthonot  24870  el2wlkonotot0  24872  usg2spthonot0  24889  rusgrasn  24945  rusgranumwlk  24957  clwlknclwlkdifs  24960  frgra1v  24998  1to2vfriswmgra  25006  1to3vfriswmgra  25007  3cyclfrgrarn1  25012  4cycl2vnunb  25017  frgrancvvdeqlem3  25032  frgrawopreglem3  25046  frgrawopreglem4  25047  frgrawopreg  25049  frg2woteqm  25059  2spotdisj  25061  2spotiundisj  25062  usg2spot2nb  25065  extwwlkfablem1  25074  clwwlkextfrlem1  25076  extwwlkfablem2  25078  numclwwlkun  25079  numclwwlkovf2ex  25086  numclwwlkovgelim  25089  numclwlk1lem2foa  25091  numclwlk1lem2f1  25094  numclwlk1lem2fo  25095  numclwwlk1  25098  numclwlk2lem2f  25103  numclwlk2lem2f1o  25105  numclwwlk5  25112  frgrareg  25117  frgraregord013  25118  friendship  25122  isgrpo  25198  opidonOLD  25324  grpomndo  25348  vcdi  25445  vcdir  25446  vcass  25447  nmosetre  25679  hlim2  26109  shscli  26235  chintcli  26249  dfch2  26325  spansncvi  26570  nmopsetretALT  26782  nmfnsetre  26796  lnopl  26833  lnfnl  26850  pjss2coi  27083  pjorthcoi  27088  pjscji  27089  pjssdif2i  27093  pjclem4a  27117  pj3lem1  27125  strlem5  27174  hstrlem5  27182  cvmdi  27243  mdslmd3i  27251  atcv1  27299  atcvat4i  27316  cdj3lem2a  27355  cdj3lem3a  27358  iuninc  27428  disji2f  27438  disjif2  27442  fmptcof2  27502  ssct  27532  xrsmulgzz  27666  ofldchr  27804  esumfzf  28075  issgon  28123  voliune  28201  volfiniune  28202  rrvsum  28393  cvmliftlem15  28743  relexprel  29057  relexpfld  29060  relexpadd  29061  relexpindlem  29062  rtrclreclem.trans  29069  rtrclreclem.min  29070  iprodefisumlem  29123  faclimlem1  29168  dfon2lem6  29220  tfisg  29284  poseq  29333  wfrlem11  29353  wfrlem12  29354  frrlem4  29390  frrlem5c  29393  frrlem11  29399  nodenselem5  29445  nocvxminlem  29450  nocvxmin  29451  idinside  29734  onsucconi  29902  wl-aleq  29988  fin2so  30040  itg2addnclem  30066  nn0prpw  30141  upixp  30220  welb  30227  sdclem2  30235  metf1o  30248  sstotbnd3  30272  isbndx  30278  ismtycnv  30298  heiborlem4  30310  bfplem1  30318  mzpexpmpt  30677  diophren  30747  expmordi  30883  rmxypos  30885  jm2.17a  30898  jm2.17b  30899  rmygeid  30902  divalgmodcl  30929  jm2.18  30930  jm2.25  30941  jm2.15nn0  30945  jm2.16nn0  30946  pwslnm  31040  isnumbasgrplem1  31050  dgraalem  31094  dvgrat  31193  radcnvrat  31195  2reurex  32186  2reu1  32191  eu2ndop1stv  32207  afvfv0bi  32237  afveu  32238  afvres  32257  aovmpt4g  32286  ndmaovass  32291  ndmaovdistr  32292  imarnf1pr  32309  f1dmvrnfibi  32312  f1vrnfibi  32313  subsubelfzo0  32338  fzoopth  32340  2ffzoeq  32341  usgra2pthspth  32351  usgra2pth  32354  usgrauvtxvd  32358  usgpredgv  32399  usgpredgvALT  32400  usgedgvadf1lem2  32414  usgedgvadf1ALTlem2  32417  usgresvm1  32443  usgfis  32446  usgresvm1ALT  32447  usgfisALT  32450  mgmpropd  32463  isassintop  32534  tpres  32554  inveq  32565  initoeu2lem0  32619  initoeu2lem1  32620  funcestrcsetclem8  32653  funcestrcsetclem9  32654  fthestrcsetc  32656  fullestrcsetc  32657  funcsetcestrclem9  32669  fthsetcestrc  32671  fullsetcestrc  32672  lidldomn1  32727  lidlmmgm  32731  2zlidl  32740  2zrngamgm  32745  2zrngmmgm  32752  rnghmsscmap  32782  rnghmsubcsetclem2  32784  rngcinv  32789  rngccatidOLD  32797  rngcinvOLD  32801  funcrngcsetc  32806  funcrngcsetcALT  32807  rhmsscmap  32828  rhmsubcsetclem2  32830  rhmsubcrngclem2  32836  ringcinv  32840  funcringcsetc  32843  funcringcsetcOLD2lem9  32852  ringccatidOLD  32860  ringcinvOLD  32864  srhmsubc  32884  rhmsubclem4  32897  srhmsubcOLD  32903  rhmsubcOLDlem4  32916  gsumpr  32950  lmodvsmdi  32975  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  lincdifsn  33025  lincsumcl  33032  lincscmcl  33033  lincext3  33057  lindslinindsimp1  33058  lindslinindsimp2lem5  33063  snlindsntor  33072  lincresunit2  33079  lincresunit3lem2  33081  lincresunit3  33082  sspwimpcf  33720  sspwimpcfVD  33721  e2ebindALT  33729  bnj228  33790  bnj1294  33876  bnj229  33942  bnj607  33974  bnj908  33989  bnj953  33997  bnj1118  34040  bnj1174  34059  bnj1388  34089  cvrat4  35167

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