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

Theorem com23 75
Description: Commutation of antecedents. Swap 2nd and 3rd. (Contributed by NM, 5-Aug-1993.) (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 38 . 2
31, 2syl9 69 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  com3r  76  com13  77  pm2.04  79  pm2.86d  96  impancom  431  dedlem0b  929  3com23  1178  exp3acom23  1407  cbv1hOLD  1954  sbiedOLD  2092  ax12indn  2235  moexex  2334  eqrdav  2421  ralrimdva  2785  ralrimdvva  2790  ceqsalt  2974  vtoclgft  2998  reu6  3126  sbciegft  3194  reuss2  3607  reupick  3611  reusv2lem3  4467  reusv3  4472  pwssun  4598  wefrc  4685  tz7.7  4716  ordtr2  4734  onmindif  4779  unizlim  4806  ssrel  4899  ssrel2  4901  ssrelrel  4911  funssres  5430  fv3  5673  fvmptt  5759  fvcofneq  5821  funfvima2  5921  isoini  5997  isopolem  6004  weniso  6013  f1ocnv2d  6281  limsssuc  6431  tfindsg  6441  limomss  6451  findsg  6473  funcnvuni  6499  f1oweALT  6530  bropopvvv  6622  f1o2ndf1  6649  frxp  6651  suppfnss  6680  onfununi  6761  tz7.49  6859  omordi  6966  omlimcl  6978  omass  6980  oeordsuc  6994  nnmordi  7031  nnmord  7032  omabs  7047  xpdom2  7365  infensuc  7448  findcard2  7511  findcard2d  7513  findcard3  7514  frfi  7516  xpfi  7542  fsuppsssupp  7593  dffi2  7620  elfiun  7627  ordiso2  7676  ordtypelem7  7685  suc11reg  7772  inf3lem2  7782  noinfep  7812  noinfepOLD  7813  cantnfle  7826  cantnflem1  7844  cantnf  7848  cantnfleOLD  7856  cantnflem1OLD  7867  cantnfOLD  7870  trcl  7895  epfrs  7898  r1sdom  7928  pr2ne  8119  dfac8alem  8146  indcardi  8158  alephordi  8191  dfac12lem3  8261  pwsdompw  8320  cofsmo  8385  cfcoflem  8388  coftr  8389  isf32lem2  8470  isf32lem9  8477  axcc3  8554  domtriomlem  8558  axdc3lem2  8567  axdc3lem4  8569  zorn2lem4  8615  zorn2lem6  8617  zorn2lem7  8618  ttukeylem6  8630  uniimadom  8655  konigthlem  8679  fpwwe2lem8  8750  tskord  8893  tskcard  8894  grupr  8910  gruiin  8923  grudomon  8930  grur1a  8932  nqereu  9044  genpn0  9118  genpcd  9121  distrlem5pr  9142  psslinpr  9146  ltaddpr  9149  ltexprlem3  9153  ltexprlem6  9156  ltapr  9160  prlem936  9162  suplem1pr  9167  axpre-sup  9282  1re  9331  ltletr  9412  dedekindle  9480  lemul12a  10133  divgt0  10143  divge0  10144  lbreu  10226  sup2  10232  infmrcl  10255  bndndx  10524  elnnz  10601  uzindOLD  10681  fzind  10685  fnn0ind  10686  uzletr  10814  uzwo  10862  uzwoOLD  10863  eqreznegel  10885  lbzbi  10888  zmax  10895  zbtwnre  10896  irradd  10922  irrmul  10923  xrltletr  11076  xrub  11219  supxrunb2  11228  iccid  11290  uzsubsubfz  11415  elfz0fzfz0  11429  fz0fzelfz0  11430  elfzmlbp  11435  fzm1  11481  fzrevral  11485  elfzodifsumelfzo  11545  ssfzoulel  11562  ssfzo12bi  11563  elfzonelfzo  11568  elfznelfzo  11571  elfznelfzob  11572  injresinjlem  11579  fleqceilz  11634  modaddmodup  11703  uzindi  11744  le2sq2  11882  sqlecan  11913  facdiv  12004  facwordi  12006  faclbnd  12007  hashle00  12099  pr2pwpr  12124  hashimarni  12142  brfi1uzind  12160  swrdnd  12267  swrdvalodm2  12274  swrdvalodm  12275  swrdswrdlem  12294  swrdswrd  12295  ccatopth2  12306  wrd2ind  12313  swrdccatin1  12315  swrdccatin12lem2a  12317  swrdccatin2  12319  swrdccatin12lem2  12321  swrdccatin12lem3  12322  swrdccat  12325  swrdccat3blem  12327  repswswrd  12363  cshwidxmod  12381  cshwidx0  12383  cau3lem  12783  caubnd  12787  climrlim2  12966  rlimuni  12969  rlimcn2  13009  mulcn2  13014  rlimno1  13072  climcau  13089  climbdd  13090  caucvg  13097  xpnnenOLD  13432  dvdsle  13518  ndvdssub  13551  gcdcllem1  13635  dvdslegcd  13640  bezoutlem4  13665  coprmdvds  13728  coprmdvds2  13729  prmfac1  13744  pcqcl  13863  prmpwdvds  13905  infpnlem1  13911  cshwshashlem1  14062  clatleglb  15236  gsmsymgrfixlem1  15869  gsmsymgreqlem2  15873  symggen  15913  psgnunilem4  15940  sylow2blem3  16058  lsmdisj2  16116  frgpnabllem1  16287  dprddisj2  16406  lssssr  16843  lss1d  16853  lspsncv0  17036  znrrg  17706  mamufacex  17988  mavmulsolcl  18060  cramerlem3  18199  uniopn  18214  opnnei  18428  neindisj2  18431  restcls  18489  restntr  18490  tgcnp  18561  subbascn  18562  iscnp4  18571  lmcnp  18612  lpcls  18672  cmpsublem  18706  cmpsub  18707  tgcmp  18708  cmpcld  18709  bwthOLD  18718  dfcon2  18727  1stcrest  18761  2ndcdisj  18764  1stccnp  18770  kgencn2  18834  txlm  18925  kqreglem1  19018  filin  19131  isfil2  19133  fgss2  19151  fgfil  19152  ufilmax  19184  ufileu  19196  filufint  19197  cfinufil  19205  elfm2  19225  rnelfmlem  19229  rnelfm  19230  fmfnfmlem2  19232  fmfnfmlem4  19234  flimopn  19252  fbflim2  19254  flffbas  19272  fclsnei  19296  flimfnfcls  19305  fclscmp  19307  ufilcmp  19309  fcfnei  19312  cnpfcf  19318  alexsubALTlem2  19324  alexsubALTlem3  19325  alexsubALTlem4  19326  alexsubALT  19327  ptcmplem4  19331  divstgplem  19395  tsmsres  19418  tsmsxp  19429  metss  19783  metcnp3  19815  ivthlem2  20636  ivthlem3  20637  ovoliunnul  20690  ovolicc2lem3  20702  dyadmax  20778  itg2le  20917  itgcn  21020  ellimc3  21054  lhop1  21186  dvfsumrlim  21203  fta1g  21380  fta1  21515  aalioulem3  21541  aalioulem4  21542  ulmcaulem  21600  ulmcau  21601  xrlimcnp  22103  cxploglim  22112  jensen  22123  lgsquad2lem2  22439  2sqlem6  22449  brbtwn2  22830  ax5seglem5  22858  axcontlem4  22892  axcontlem10  22898  usgranloopv  22976  usgranloop  22977  usgra2edg  22980  usgraedg4  22984  usgra1v  22987  usgraidx2vlem2  22989  usgrafisindb0  23000  usgrafisindb1  23001  usgrares1  23002  cusgrarn  23046  cusgrares  23059  cusgrasize2inds  23064  cusgrafi  23069  sizeusglecusg  23073  usgrnloop  23141  1pthoncl  23170  wlkdvspthlem  23185  wlkdvspth  23186  cyclnspth  23196  fargshiftfo  23203  fargshiftfva  23204  usgrcyclnl1  23205  nvnencycllem  23208  constr3trllem2  23216  4cycl4dv  23232  eupatrl  23268  rngoueqz  23596  nmoub3i  23852  ipasslem5  23914  htthlem  23998  ocin  24378  spansneleq  24652  spansnss  24653  elspansn4  24655  h1datomi  24663  nmopub2tALT  24992  nmfnleub2  25009  hstel2  25302  cvnbtwn  25369  spansncv2  25376  dmdmd  25383  dmdbr3  25388  dmdbr4  25389  dmdbr5  25391  mdsl0  25393  mdexchi  25418  cvexchlem  25451  atcv1  25463  atomli  25465  atcvatlem  25468  atcvat2i  25470  chirredi  25477  mdsymlem3  25488  mdsymlem4  25489  sumdmdii  25498  sumdmdlem  25501  cdj1i  25516  ssrelf  25625  f1o3d  25628  cvxpcon  26834  ghomf1olem  27015  fundmpss  27279  dfon2lem6  27303  dfon2lem8  27305  dfon2lem9  27306  dfon2  27307  predpo  27347  trpredrec  27404  soseq  27417  wfr3g  27425  wfrlem12  27437  wzel  27463  frr3g  27469  frrlem11  27482  nodenselem5  27528  nodenselem7  27530  nodenselem8  27531  nofulllem5  27549  colinearxfr  27808  btwnconn1lem11  27830  lineintmo  27890  ordcmp  27996  ee7.2aOLD  28010  finixpnum  28085  bddiblnc  28133  ftc1anc  28146  trer  28182  elicc3  28183  finminlem  28184  nn0prpwlem  28188  fnessref  28236  comppfsc  28250  neibastop2  28253  fgmin  28262  tailfb  28269  fdc  28312  heibor1lem  28379  ghomco  28419  unichnidl  28502  dmncan1  28547  pell1qrgap  28888  dford3lem1  29048  hbtlem5  29157  sbiota1  29361  funressnfv  29708  ralxfrd2  29811  uzuzle  29864  el2fzo  29886  fzoopth  29887  elfzom1elp1fzo  29892  modfsummod  29919  lswn0  29932  usgra2wlkspthlem2  29971  usgra2pthlem1  29974  wwlknimp  29995  wlkiswwlk2  30005  wwlknred  30029  wwlknext  30030  wwlknextbi  30031  wwlkextwrd  30034  wwlkextinj  30036  el2wlkonot  30062  usg2wotspth  30077  usg2spthonot  30081  usg2spthonot0  30082  clwwlkgt0  30108  clwwlknprop  30109  clwlkisclwwlklem2a4  30120  clwlkisclwwlklem2a  30121  clwlkisclwwlklem0  30124  clwwlkf  30130  wwlkext2clwwlk  30139  zm1nn  30142  clwwisshclwwlem1  30143  erclwwlktr0  30153  erclwwlkeqlen  30156  erclwwlksym  30158  cshwlemma1  30163  Lemma2  30167  erclwwlkneqlen  30172  erclwwlknsym  30174  wlkp1lenfislenp  30186  clwlkfclwwlk  30191  clwlkfoclwwlk  30192  usgfiregdegfi  30202  nbhashuvtx1  30207  rusgraprop4  30230  wwlkextproplem2  30235  wwlkextproplem3  30236  3vfriswmgra  30271  1to2vfriswmgra  30272  1to3vfriswmgra  30273  3cyclfrgrarn  30279  n4cyclfrgra  30284  4cyclusnfrgra  30285  frgranbnb  30286  frgrancvvdeqlemB  30305  frg2wot1  30324  frg2woteqm  30326  frg2woteq  30327  usg2spot2nb  30332  2spotmdisj  30335  usgreghash2spot  30336  frgregordn0  30337  numclwwlkovf2ex  30353  numclwlk1lem2fo  30362  numclwlk2lem2f  30370  numclwwlk8  30382  frgrareg  30384  frgraregord013  30385  frgraogt3nreg  30387  ztprmneprm  30411  lmod0rng  30439  lcoel0  30546  linindslinci  30566  lindslinindimp2lem4  30579  lindslinindsimp2lem5  30580  snlindsntor  30589  ldepspr  30591  lincresunit2  30596  ad5ant13  30744  ad5ant14  30745  ad5ant15  30746  ad5ant134  30756  ad5ant135  30757  ad5ant145  30758  19.41rg  30836  ee223  30934  bj-ceqsalt  31856  lshpdisj  32069  lub0N  32271  glb0N  32275  leat2  32376  hlrelat2  32484  cvrexchlem  32500  cvratlem  32502  atcvrj0  32509  cvrat2  32510  snatpsubN  32831  linepsubN  32833  pmaple  32842  pmapsub  32849  elpaddn0  32881  paddasslem5  32905  trlval2  33244  cdlemn11pre  34292  dihord2pre  34307  mapdordlem2  34719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator