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  a2and  811  dedlem0b  953  3com23  1202  ax12indn  2273  moexex  2363  eqrdavOLD  2456  ralrimdvaOLD  2876  ralrimdvva  2881  ceqsalt  3132  vtoclgft  3157  reu6  3288  sbciegft  3358  reuss2  3777  reupick  3781  reusv2lem3  4655  reusv3  4660  pwssun  4791  wefrc  4878  tz7.7  4909  ordtr2  4927  onmindif  4972  unizlim  4999  ssrel  5096  ssrel2  5098  ssrelrel  5108  funssres  5633  fv3  5884  fvmptt  5971  fveqdmss  6026  fvcofneq  6039  fmptsnd  6093  funfvima2  6148  isoini  6234  isopolem  6241  weniso  6250  f1ocnv2d  6526  limsssuc  6685  tfindsg  6695  limomss  6705  findsg  6727  funcnvuni  6753  f1oweALT  6784  bropopvvv  6880  f1o2ndf1  6908  frxp  6910  suppfnss  6944  onfununi  7031  tz7.49  7129  omordi  7234  omlimcl  7246  omass  7248  oeordsuc  7262  nnmordi  7299  nnmord  7300  omabs  7315  xpdom2  7632  infensuc  7715  findcard2  7780  findcard2d  7782  findcard3  7783  frfi  7785  xpfi  7811  fsuppres  7874  dffi2  7903  elfiun  7910  ordiso2  7961  ordtypelem7  7970  suc11reg  8057  inf3lem2  8067  noinfep  8097  noinfepOLD  8098  cantnfle  8111  cantnflem1  8129  cantnf  8133  cantnfleOLD  8141  cantnflem1OLD  8152  cantnfOLD  8155  trcl  8180  epfrs  8183  r1sdom  8213  pr2ne  8404  dfac8alem  8431  indcardi  8443  alephordi  8476  dfac12lem3  8546  pwsdompw  8605  cofsmo  8670  cfcoflem  8673  coftr  8674  isf32lem2  8755  isf32lem9  8762  axcc3  8839  domtriomlem  8843  axdc3lem2  8852  axdc3lem4  8854  zorn2lem4  8900  zorn2lem6  8902  zorn2lem7  8903  ttukeylem6  8915  uniimadom  8940  konigthlem  8964  fpwwe2lem8  9036  tskord  9179  tskcard  9180  grupr  9196  gruiin  9209  grudomon  9216  grur1a  9218  nqereu  9328  genpn0  9402  genpcd  9405  distrlem5pr  9426  psslinpr  9430  ltaddpr  9433  ltexprlem3  9437  ltexprlem6  9440  ltapr  9444  prlem936  9446  suplem1pr  9451  axpre-sup  9567  1re  9616  ltletr  9697  dedekindle  9766  lemul12a  10425  divgt0  10435  divge0  10436  lbreu  10518  sup2  10524  infmrcl  10547  bndndx  10819  elnnz  10899  uzindOLD  10982  fzind  10987  fnn0ind  10988  uzwo  11173  uzwoOLD  11174  eqreznegel  11196  lbzbi  11199  zmax  11208  zbtwnre  11209  irradd  11235  irrmul  11236  xrltletr  11389  xrub  11532  supxrunb2  11541  iccid  11603  uzsubsubfz  11736  fzrevral  11792  elfz0fzfz0  11808  fz0fzelfz0  11809  elfzmlbp  11815  elfzodifsumelfzo  11882  ssfzoulel  11906  ssfzo12bi  11907  elfzonelfzo  11912  elfznelfzo  11915  elfznelfzob  11916  injresinjlem  11925  fleqceilz  11981  modaddmodup  12050  uzindi  12091  suppssfz  12100  mptnn0fsuppr  12105  le2sq2  12243  sqlecan  12274  facdiv  12365  facwordi  12367  faclbnd  12368  hashle00  12465  hashimarni  12497  pr2pwpr  12520  brfi1uzind  12532  swrdnd  12657  swrdvalodm2  12664  swrdvalodm  12665  swrdswrdlem  12684  swrdswrd  12685  ccatopth2  12696  wrd2ind  12703  reuccats1lem  12705  swrdccatin1  12708  swrdccatin12lem2a  12710  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccatin12lem3  12715  swrdccat  12718  swrdccat3blem  12720  repswswrd  12756  cshwidxmod  12774  cshwidx0  12776  2cshwcshw  12793  cshwcsh2id  12796  cau3lem  13187  caubnd  13191  climrlim2  13370  rlimuni  13373  rlimcn2  13413  mulcn2  13418  rlimno1  13476  climcau  13493  climbdd  13494  caucvg  13501  modfsummod  13608  xpnnenOLD  13943  dvdsle  14031  ndvdssub  14065  gcdcllem1  14149  dvdslegcd  14154  bezoutlem4  14179  coprmdvds  14243  coprmdvds2  14244  prmfac1  14259  pcqcl  14380  prmpwdvds  14422  infpnlem1  14428  cshwshashlem1  14580  clatleglb  15756  gsmsymgrfixlem1  16452  gsmsymgreqlem2  16456  symggen  16495  psgnunilem4  16522  sylow2blem3  16642  lsmdisj2  16700  frgpnabllem1  16877  dprddisj2  17087  dprddisj2OLD  17088  f1rhm0to0ALT  17390  lssssr  17599  lss1d  17609  lspsncv0  17792  mplcoe5lem  18130  cply1mul  18335  coe1fzgsumdlem  18343  gsummoncoe1  18346  evl1gsumdlem  18392  znrrg  18604  mamufacex  18891  dmatelnd  18998  scmataddcl  19018  scmatsubcl  19019  scmatmulcl  19020  smatvscl  19026  mavmulsolcl  19053  mdetdiagid  19102  cramerlem3  19191  pmatcoe1fsupp  19202  cpmatacl  19217  cpmatmcllem  19219  mp2pm2mplem4  19310  chpscmat  19343  chfacfisf  19355  chfacfisfcpmat  19356  uniopn  19406  opnnei  19621  neindisj2  19624  restcls  19682  restntr  19683  tgcnp  19754  subbascn  19755  iscnp4  19764  lmcnp  19805  lpcls  19865  cmpsublem  19899  cmpsub  19900  tgcmp  19901  cmpcld  19902  bwthOLD  19911  dfcon2  19920  1stcrest  19954  2ndcdisj  19957  1stccnp  19963  comppfsc  20033  kgencn2  20058  txlm  20149  kqreglem1  20242  filin  20355  isfil2  20357  fgss2  20375  fgfil  20376  ufilmax  20408  ufileu  20420  filufint  20421  cfinufil  20429  elfm2  20449  rnelfmlem  20453  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem4  20458  flimopn  20476  fbflim2  20478  flffbas  20496  fclsnei  20520  flimfnfcls  20529  fclscmp  20531  ufilcmp  20533  fcfnei  20536  cnpfcf  20542  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  ptcmplem4  20555  qustgplem  20619  tsmsresOLD  20645  tsmsres  20646  tsmsxp  20657  metss  21011  metcnp3  21043  ivthlem2  21864  ivthlem3  21865  ovoliunnul  21918  ovolicc2lem3  21930  dyadmax  22007  itg2le  22146  itgcn  22249  ellimc3  22283  lhop1  22415  dvfsumrlim  22432  fta1g  22568  fta1  22704  aalioulem3  22730  aalioulem4  22731  ulmcaulem  22789  ulmcau  22790  xrlimcnp  23298  cxploglim  23307  jensen  23318  lgsquad2lem2  23634  2sqlem6  23644  brbtwn2  24208  ax5seglem5  24236  axcontlem4  24270  axcontlem10  24276  usgranloopv  24378  usgranloop  24379  usgra2edg  24382  usgraedg4  24387  usgra1v  24390  usgraidx2vlem2  24392  usgrafisindb0  24408  usgrafisindb1  24409  usgrares1  24410  cusgrarn  24459  cusgrares  24472  cusgrasize2inds  24477  cusgrafi  24482  sizeusglecusg  24486  usgrnloop  24565  1pthoncl  24594  wlkdvspthlem  24609  wlkdvspth  24610  usgra2wlkspthlem2  24620  cyclnspth  24631  fargshiftfo  24638  fargshiftfva  24639  usgrcyclnl1  24640  nvnencycllem  24643  constr3trllem2  24651  4cycl4dv  24667  wwlknimp  24687  wlkiswwlk2  24697  wwlknred  24723  wwlknext  24724  wwlknextbi  24725  wwlkextwrd  24728  wwlkextinj  24730  wwlkextproplem2  24742  wwlkextproplem3  24743  clwwlkgt0  24771  clwwlknprop  24772  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem0  24788  clwwlkf  24794  wwlkext2clwwlk  24803  clwwisshclwwlem1  24805  erclwwlkeqlen  24812  erclwwlksym  24814  clwwlknscsh  24819  erclwwlkneqlen  24824  erclwwlknsym  24826  wlklenvclwlk  24839  clwlkfclwwlk  24844  clwlkfoclwwlk  24845  el2wlkonot  24869  usg2wotspth  24884  usg2spthonot  24888  usg2spthonot0  24889  usgfiregdegfi  24911  nbhashuvtx1  24915  rusgraprop4  24944  eupatrl  24968  3vfriswmgra  25005  1to2vfriswmgra  25006  1to3vfriswmgra  25007  3cyclfrgrarn  25013  n4cyclfrgra  25018  4cyclusnfrgra  25019  frgranbnb  25020  frgrancvvdeqlemB  25038  frg2wot1  25057  frg2woteqm  25059  frg2woteq  25060  usg2spot2nb  25065  2spotmdisj  25068  usgreghash2spot  25069  frgregordn0  25070  numclwwlkovf2ex  25086  numclwlk1lem2fo  25095  numclwlk2lem2f  25103  numclwwlk8  25115  frgrareg  25117  frgraregord013  25118  frgraogt3nreg  25120  rngoueqz  25432  nmoub3i  25688  ipasslem5  25750  htthlem  25834  ocin  26214  spansneleq  26488  spansnss  26489  elspansn4  26491  h1datomi  26499  nmopub2tALT  26828  nmfnleub2  26845  hstel2  27138  cvnbtwn  27205  spansncv2  27212  dmdmd  27219  dmdbr3  27224  dmdbr4  27225  dmdbr5  27227  mdsl0  27229  mdexchi  27254  cvexchlem  27287  atcv1  27299  atomli  27301  atcvatlem  27304  atcvat2i  27306  chirredi  27313  mdsymlem3  27324  mdsymlem4  27325  sumdmdii  27334  sumdmdlem  27337  cdj1i  27352  ssrelf  27466  f1o3d  27471  cvxpcon  28687  mrsubccat  28878  msubvrs  28920  ghomf1olem  29034  fundmpss  29196  dfon2lem6  29220  dfon2lem8  29222  dfon2lem9  29223  dfon2  29224  predpo  29264  trpredrec  29321  soseq  29334  wfr3g  29342  wfrlem12  29354  wzel  29380  frr3g  29386  frrlem11  29399  nodenselem5  29445  nodenselem7  29447  nodenselem8  29448  nofulllem5  29466  colinearxfr  29725  btwnconn1lem11  29747  lineintmo  29807  ordcmp  29912  ee7.2aOLD  29926  wl-mo3t  30021  finixpnum  30038  bddiblnc  30085  ftc1anc  30098  trer  30134  elicc3  30135  finminlem  30136  nn0prpwlem  30140  fnessref  30175  neibastop2  30179  fgmin  30188  tailfb  30195  fdc  30238  heibor1lem  30305  ghomco  30345  unichnidl  30428  dmncan1  30473  pell1qrgap  30810  dford3lem1  30968  hbtlem5  31077  sbiota1  31341  funressnfv  32213  ralxfrd2  32303  zm1nn  32325  el2fzo  32339  fzoopth  32340  lswn0  32343  usgra2pthlem1  32353  usgpredgv  32399  usgpredgvALT  32400  cictr  32589  initoeu2lem1  32620  initoeu2  32622  lmod0rng  32674  nzerooringczr  32880  ztprmneprm  32936  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  lcoel0  33029  linindslinci  33049  lindslinindimp2lem4  33062  lindslinindsimp2lem5  33063  snlindsntor  33072  ldepspr  33074  lincresunit2  33079  aacllem  33216  ad5ant13  33233  ad5ant14  33234  ad5ant15  33235  ad5ant134  33245  ad5ant135  33246  ad5ant145  33247  19.41rg  33323  ee223  33420  bj-ceqsalt0  34449  bj-ceqsalt1  34450  lshpdisj  34712  lub0N  34914  glb0N  34918  leat2  35019  hlrelat2  35127  cvrexchlem  35143  cvratlem  35145  atcvrj0  35152  cvrat2  35153  snatpsubN  35474  linepsubN  35476  pmaple  35485  pmapsub  35492  elpaddn0  35524  paddasslem5  35548  trlval2  35888  cdlemn11pre  36937  dihord2pre  36952  mapdordlem2  37364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator