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

Theorem com13 80
 Description: Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com3.1
Assertion
Ref Expression
com13

Proof of Theorem com13
StepHypRef Expression
1 com3.1 . . 3
21com3r 79 . 2
32com23 78 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4 This theorem is referenced by:  com24  87  imim12  97  an13s  803  an31s  806  meredith  1472  otiunsndisj  4758  funopg  5625  eldmrexrnb  6038  fvn0fvelrn  6088  peano5  6723  f1o2ndf1  6908  suppimacnv  6929  omordi  7234  omeulem1  7250  brecop  7423  isinf  7753  fiint  7817  carduni  8383  dfac5  8530  dfac2  8532  cofsmo  8670  cfcoflem  8673  domtriomlem  8843  axdc3lem2  8852  nqereu  9328  squeeze0  10473  zmax  11208  xrsupsslem  11527  xrinfmsslem  11528  supxrunb1  11540  supxrunb2  11541  difreicc  11681  elfz0ubfz0  11807  elfz0fzfz0  11808  fz0fzelfz0  11809  fz0fzdiffz0  11812  fzo1fzo0n0  11864  elfzodifsumelfzo  11882  ssfzo12  11905  ssfzo12bi  11907  elfznelfzo  11915  injresinjlem  11925  injresinj  11926  uzindi  12091  ssnn0fi  12094  suppssfz  12100  facwordi  12367  hasheqf1oi  12424  hashf1rn  12425  hash2prde  12516  swrdnd  12657  swrdvalodm2  12664  swrdswrdlem  12684  swrdswrd  12685  wrd2ind  12703  reuccats1lem  12705  swrdccatin1  12708  swrdccatin12lem2  12714  swrdccat  12718  repsdf2  12750  cshwidx0  12776  cshweqrep  12789  2cshwcshw  12793  cshwcsh2id  12796  swrdco  12803  wwlktovfo  12896  sqrt2irr  13982  symgfix2  16441  gsmsymgreqlem2  16456  psgnunilem4  16522  01eq0ring  17920  cply1mul  18335  gsummoncoe1  18346  mamufacex  18891  matecl  18927  gsummatr01lem4  19160  gsummatr01  19161  mp2pm2mplem4  19310  chfacfscmul0  19359  chfacfpmmul0  19363  cayhamlem1  19367  bwthOLD  19911  fbunfip  20370  usgranloopv  24378  usgraedg4  24387  usgraidx2vlem2  24392  usgrafisbase  24414  nbgra0nb  24429  nbgraf1olem3  24443  nbgraf1olem5  24445  nbcusgra  24463  cusgrasize2inds  24477  cusgrafi  24482  usgrasscusgra  24483  sizeusglecusglem1  24484  sizeusglecusg  24486  uvtxnbgra  24493  spthonepeq  24589  1pthoncl  24594  wlkdvspthlem  24609  usgra2adedgspthlem2  24612  usgra2wlkspthlem1  24619  usgra2wlkspth  24621  cyclnspth  24631  fargshiftf1  24637  usgrcyclnl2  24641  nvnencycllem  24643  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  usg2wlkeq  24708  wwlknextbi  24725  wwlknredwwlkn0  24727  wwlkextinj  24730  clwwlkgt0  24771  clwlkisclwwlklem2a1  24779  clwlkisclwwlklem2fv2  24783  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwwlkext2edg  24802  clwwisshclww  24807  erclwwlktr  24815  usg2cwwk2dif  24820  erclwwlkntr  24827  clwlkf1clwwlklem  24849  el2wlkonotot0  24872  usg2wlkonot  24883  usg2wotspth  24884  usgfidegfi  24910  hashnbgravdg  24913  frgraunss  24995  frgra3vlem1  25000  3cyclfrgrarn1  25012  3cyclfrgrarn  25013  4cycl2vnunb  25017  frgranbnb  25020  vdn0frgrav2  25023  vdn1frgrav2  25025  usgn0fidegnn0  25029  frgrancvvdeqlemB  25038  frgrawopreglem2  25045  frg2wot1  25057  usg2spot2nb  25065  2spotmdisj  25068  clwwlkextfrlem1  25076  extwwlkfablem2  25078  numclwlk1lem2fo  25095  frgrareggt1  25116  frgrareg  25117  friendshipgt3  25121  grpomndo  25348  rngoueqz  25432  zerdivemp1  25436  rngoridfz  25437  shmodsi  26307  kbass6  27040  mdsymlem6  27327  mdsymlem7  27328  cdj3lem2a  27355  cdj3lem3a  27358  predpo  29264  zerdivemp1x  30358  funressnfv  32213  funbrafv  32243  otiunsndisjX  32301  ssfz12  32330  fzoopth  32340  usgra2pthspth  32351  usgra2pth  32354  initoeu2lem1  32620  lidldomn1  32727  2zrngamgm  32745  rngccatidOLD  32797  ringccatidOLD  32860  nzerooringczr  32880  scmsuppss  32965  ply1mulgsumlem1  32986  lincsumcl  33032  ellcoellss  33036  lindslinindsimp1  33058  lindslinindimp2lem1  33059  3imp31  33340  eel12131  33506  tratrbVD  33661  2uasbanhVD  33711  elpcliN  35617 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
 Copyright terms: Public domain W3C validator