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

Theorem com23 78
Description: Commutation of antecedents. Swap 2nd and 3rd. (Contributed by NM, 27-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com3.1
Assertion
Ref Expression
com23

Proof of Theorem com23
StepHypRef Expression
1 com3.1 . 2
2 pm2.27 39 . 2
31, 2syl9 71 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  com3r  79  com13  80  pm2.04  82  pm2.86d  99  expcomd  438  impancom  440  dedlem0b  944  3com23  1194  cbv1hOLD  1975  sbiedOLD  2113  ax12indn  2253  moexex  2358  eqrdavOLD  2453  ralrimdva  2914  ralrimdvva  2919  ceqsalt  3104  vtoclgft  3129  reu6  3258  sbciegft  3328  reuss2  3744  reupick  3748  reusv2lem3  4612  reusv3  4617  pwssun  4744  wefrc  4831  tz7.7  4862  ordtr2  4880  onmindif  4925  unizlim  4952  ssrel  5045  ssrel2  5047  ssrelrel  5057  funssres  5577  fv3  5826  fvmptt  5912  fvcofneq  5974  fmptsnd  6025  funfvima2  6078  isoini  6160  isopolem  6167  weniso  6176  f1ocnv2d  6444  limsssuc  6594  tfindsg  6604  limomss  6614  findsg  6636  funcnvuni  6663  f1oweALT  6694  bropopvvv  6786  f1o2ndf1  6814  frxp  6816  suppfnss  6848  onfununi  6936  tz7.49  7034  omordi  7139  omlimcl  7151  omass  7153  oeordsuc  7167  nnmordi  7204  nnmord  7205  omabs  7220  xpdom2  7540  infensuc  7623  findcard2  7687  findcard2d  7689  findcard3  7690  frfi  7692  xpfi  7718  fsuppres  7780  dffi2  7809  elfiun  7816  ordiso2  7866  ordtypelem7  7875  suc11reg  7962  inf3lem2  7972  noinfep  8002  noinfepOLD  8003  cantnfle  8016  cantnflem1  8034  cantnf  8038  cantnfleOLD  8046  cantnflem1OLD  8057  cantnfOLD  8060  trcl  8085  epfrs  8088  r1sdom  8118  pr2ne  8309  dfac8alem  8336  indcardi  8348  alephordi  8381  dfac12lem3  8451  pwsdompw  8510  cofsmo  8575  cfcoflem  8578  coftr  8579  isf32lem2  8660  isf32lem9  8667  axcc3  8744  domtriomlem  8748  axdc3lem2  8757  axdc3lem4  8759  zorn2lem4  8805  zorn2lem6  8807  zorn2lem7  8808  ttukeylem6  8820  uniimadom  8845  konigthlem  8869  fpwwe2lem8  8941  tskord  9084  tskcard  9085  grupr  9101  gruiin  9114  grudomon  9121  grur1a  9123  nqereu  9235  genpn0  9309  genpcd  9312  distrlem5pr  9333  psslinpr  9337  ltaddpr  9340  ltexprlem3  9344  ltexprlem6  9347  ltapr  9351  prlem936  9353  suplem1pr  9358  axpre-sup  9473  1re  9522  ltletr  9603  dedekindle  9671  lemul12a  10324  divgt0  10334  divge0  10335  lbreu  10417  sup2  10423  infmrcl  10446  bndndx  10716  elnnz  10794  uzindOLD  10874  fzind  10878  fnn0ind  10879  uzletr  11008  uzwo  11056  uzwoOLD  11057  eqreznegel  11079  lbzbi  11082  zmax  11089  zbtwnre  11090  irradd  11116  irrmul  11117  xrltletr  11270  xrub  11413  supxrunb2  11422  iccid  11484  uzsubsubfz  11616  elfz0fzfz0  11630  fz0fzelfz0  11631  elfzmlbp  11636  fzm1  11685  fzrevral  11689  elfzodifsumelfzo  11749  ssfzoulel  11766  ssfzo12bi  11767  elfzonelfzo  11772  elfznelfzo  11775  elfznelfzob  11776  injresinjlem  11783  fleqceilz  11838  modaddmodup  11907  uzindi  11948  suppssfz  11957  mptnn0fsuppr  11962  le2sq2  12098  sqlecan  12129  facdiv  12220  facwordi  12222  faclbnd  12223  hashle00  12316  pr2pwpr  12341  hashimarni  12359  brfi1uzind  12377  swrdnd  12484  swrdvalodm2  12491  swrdvalodm  12492  swrdswrdlem  12511  swrdswrd  12512  ccatopth2  12523  wrd2ind  12530  swrdccatin1  12532  swrdccatin12lem2a  12534  swrdccatin2  12536  swrdccatin12lem2  12538  swrdccatin12lem3  12539  swrdccat  12542  swrdccat3blem  12544  repswswrd  12580  cshwidxmod  12598  cshwidx0  12600  cau3lem  13000  caubnd  13004  climrlim2  13183  rlimuni  13186  rlimcn2  13226  mulcn2  13231  rlimno1  13289  climcau  13306  climbdd  13307  caucvg  13314  xpnnenOLD  13650  dvdsle  13736  ndvdssub  13769  gcdcllem1  13853  dvdslegcd  13858  bezoutlem4  13883  coprmdvds  13946  coprmdvds2  13947  prmfac1  13962  pcqcl  14081  prmpwdvds  14123  infpnlem1  14129  cshwshashlem1  14280  clatleglb  15455  gsmsymgrfixlem1  16091  gsmsymgreqlem2  16095  symggen  16135  psgnunilem4  16162  sylow2blem3  16282  lsmdisj2  16340  frgpnabllem1  16512  dprddisj2  16712  dprddisj2OLD  16713  f1rhm0to0ALT  17005  lssssr  17210  lss1d  17220  lspsncv0  17403  mplcoe5lem  17724  cply1mul  17929  coe1fzgsumdlem  17937  gsummoncoe1  17940  evl1gsumdlem  17983  znrrg  18191  mamufacex  18478  dmatelnd  18586  scmatsubcl  18605  scmatmulcl  18606  mavmulsolcl  18625  mdetdiagid  18674  cramerlem3  18763  pmatcoe1fsupp  18774  cpmatacl  18789  cpmatmcllem  18791  mp2pm2mplem4  18881  uniopn  18909  opnnei  19123  neindisj2  19126  restcls  19184  restntr  19185  tgcnp  19256  subbascn  19257  iscnp4  19266  lmcnp  19307  lpcls  19367  cmpsublem  19401  cmpsub  19402  tgcmp  19403  cmpcld  19404  bwthOLD  19413  dfcon2  19422  1stcrest  19456  2ndcdisj  19459  1stccnp  19465  kgencn2  19529  txlm  19620  kqreglem1  19713  filin  19826  isfil2  19828  fgss2  19846  fgfil  19847  ufilmax  19879  ufileu  19891  filufint  19892  cfinufil  19900  elfm2  19920  rnelfmlem  19924  rnelfm  19925  fmfnfmlem2  19927  fmfnfmlem4  19929  flimopn  19947  fbflim2  19949  flffbas  19967  fclsnei  19991  flimfnfcls  20000  fclscmp  20002  ufilcmp  20004  fcfnei  20007  cnpfcf  20013  alexsubALTlem2  20019  alexsubALTlem3  20020  alexsubALTlem4  20021  alexsubALT  20022  ptcmplem4  20026  divstgplem  20090  tsmsresOLD  20116  tsmsres  20117  tsmsxp  20128  metss  20482  metcnp3  20514  ivthlem2  21335  ivthlem3  21336  ovoliunnul  21389  ovolicc2lem3  21401  dyadmax  21478  itg2le  21617  itgcn  21720  ellimc3  21754  lhop1  21886  dvfsumrlim  21903  fta1g  22039  fta1  22174  aalioulem3  22200  aalioulem4  22201  ulmcaulem  22259  ulmcau  22260  xrlimcnp  22762  cxploglim  22771  jensen  22782  lgsquad2lem2  23098  2sqlem6  23108  brbtwn2  23620  ax5seglem5  23648  axcontlem4  23682  axcontlem10  23688  usgranloopv  23766  usgranloop  23767  usgra2edg  23770  usgraedg4  23774  usgra1v  23777  usgraidx2vlem2  23779  usgrafisindb0  23790  usgrafisindb1  23791  usgrares1  23792  cusgrarn  23836  cusgrares  23849  cusgrasize2inds  23854  cusgrafi  23859  sizeusglecusg  23863  usgrnloop  23931  1pthoncl  23960  wlkdvspthlem  23975  wlkdvspth  23976  cyclnspth  23986  fargshiftfo  23993  fargshiftfva  23994  usgrcyclnl1  23995  nvnencycllem  23998  constr3trllem2  24006  4cycl4dv  24022  eupatrl  24058  rngoueqz  24386  nmoub3i  24642  ipasslem5  24704  htthlem  24788  ocin  25168  spansneleq  25442  spansnss  25443  elspansn4  25445  h1datomi  25453  nmopub2tALT  25782  nmfnleub2  25799  hstel2  26092  cvnbtwn  26159  spansncv2  26166  dmdmd  26173  dmdbr3  26178  dmdbr4  26179  dmdbr5  26181  mdsl0  26183  mdexchi  26208  cvexchlem  26241  atcv1  26253  atomli  26255  atcvatlem  26258  atcvat2i  26260  chirredi  26267  mdsymlem3  26278  mdsymlem4  26279  sumdmdii  26288  sumdmdlem  26291  cdj1i  26306  ssrelf  26413  f1o3d  26416  cvxpcon  27587  ghomf1olem  27769  fundmpss  28033  dfon2lem6  28057  dfon2lem8  28059  dfon2lem9  28060  dfon2  28061  predpo  28101  trpredrec  28158  soseq  28171  wfr3g  28179  wfrlem12  28191  wzel  28217  frr3g  28223  frrlem11  28236  nodenselem5  28282  nodenselem7  28284  nodenselem8  28285  nofulllem5  28303  colinearxfr  28562  btwnconn1lem11  28584  lineintmo  28644  ordcmp  28749  ee7.2aOLD  28763  wl-mo3t  28857  finixpnum  28874  bddiblnc  28922  ftc1anc  28935  trer  28971  elicc3  28972  finminlem  28973  nn0prpwlem  28977  fnessref  29025  comppfsc  29039  neibastop2  29042  fgmin  29051  tailfb  29058  fdc  29101  heibor1lem  29168  ghomco  29208  unichnidl  29291  dmncan1  29336  pell1qrgap  29675  dford3lem1  29835  hbtlem5  29944  sbiota1  30148  funressnfv  30911  ralxfrd2  31014  uzuzle  31067  el2fzo  31089  fzoopth  31090  elfzom1elp1fzo  31095  modfsummod  31122  lswn0  31135  usgra2wlkspthlem2  31174  usgra2pthlem1  31177  wwlknimp  31198  wlkiswwlk2  31208  wwlknred  31232  wwlknext  31233  wwlknextbi  31234  wwlkextwrd  31237  wwlkextinj  31239  el2wlkonot  31265  usg2wotspth  31280  usg2spthonot  31284  usg2spthonot0  31285  clwwlkgt0  31311  clwwlknprop  31312  clwlkisclwwlklem2a4  31323  clwlkisclwwlklem2a  31324  clwlkisclwwlklem0  31327  clwwlkf  31333  wwlkext2clwwlk  31342  zm1nn  31345  clwwisshclwwlem1  31346  erclwwlktr0  31356  erclwwlkeqlen  31359  erclwwlksym  31361  cshwlemma1  31366  Lemma2  31370  erclwwlkneqlen  31375  erclwwlknsym  31377  wlkp1lenfislenp  31389  clwlkfclwwlk  31394  clwlkfoclwwlk  31395  usgfiregdegfi  31405  nbhashuvtx1  31410  rusgraprop4  31433  wwlkextproplem2  31438  wwlkextproplem3  31439  3vfriswmgra  31474  1to2vfriswmgra  31475  1to3vfriswmgra  31476  3cyclfrgrarn  31482  n4cyclfrgra  31487  4cyclusnfrgra  31488  frgranbnb  31489  frgrancvvdeqlemB  31508  frg2wot1  31527  frg2woteqm  31529  frg2woteq  31530  usg2spot2nb  31535  2spotmdisj  31538  usgreghash2spot  31539  frgregordn0  31540  numclwwlkovf2ex  31556  numclwlk1lem2fo  31565  numclwlk2lem2f  31573  numclwwlk8  31585  frgrareg  31587  frgraregord013  31588  frgraogt3nreg  31590  ztprmneprm  31613  lmod0rng  31647  ply1mulgsumlem1  31688  ply1mulgsumlem2  31689  lcoel0  31734  linindslinci  31754  lindslinindimp2lem4  31767  lindslinindsimp2lem5  31768  snlindsntor  31777  ldepspr  31779  lincresunit2  31784  chpscmat  31840  chfacfisf  31852  chfacfisfcpmat  31853  ad5ant13  32011  ad5ant14  32012  ad5ant15  32013  ad5ant134  32023  ad5ant135  32024  ad5ant145  32025  19.41rg  32102  ee223  32199  bj-ceqsalt0  33229  bj-ceqsalt1  33230  lshpdisj  33483  lub0N  33685  glb0N  33689  leat2  33790  hlrelat2  33898  cvrexchlem  33914  cvratlem  33916  atcvrj0  33923  cvrat2  33924  snatpsubN  34245  linepsubN  34247  pmaple  34256  pmapsub  34263  elpaddn0  34295  paddasslem5  34319  trlval2  34658  cdlemn11pre  35706  dihord2pre  35721  mapdordlem2  36133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator