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

Theorem com24 87
Description: Commutation of antecedents. Swap 2nd and 4th. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com4.1
Assertion
Ref Expression
com24

Proof of Theorem com24
StepHypRef Expression
1 com4.1 . . 3
21com4t 85 . 2
32com13 80 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  com25  91  imim12  97  a2andOLD  812  fveqdmss  6026  tfrlem9  7073  omordi  7234  nnmordi  7299  fundmen  7609  pssnn  7758  fiint  7817  infssuni  7831  cfcoflem  8673  fin1a2lem10  8810  axdc3lem2  8852  zorn2lem7  8903  fpwwe2lem12  9040  genpnnp  9404  mulgt0sr  9503  nn01to3  11204  elfzodifsumelfzo  11882  ssfzo12  11905  elfznelfzo  11915  injresinjlem  11925  injresinj  11926  ssnn0fi  12094  expcan  12218  ltexp2  12219  hashgt12el2  12482  brfi1uzind  12532  swrdswrdlem  12684  swrdswrd  12685  wrd2ind  12703  swrdccatin1  12708  cshwlen  12770  2cshwcshw  12793  cshwcsh2id  12796  infpnlem1  14428  cshwshashlem1  14580  grpinveu  16084  mulgass2  17247  lss1d  17609  cply1mul  18335  gsummoncoe1  18346  mp2pm2mplem4  19310  chpscmat  19343  chcoeffeq  19387  cnpnei  19765  hausnei2  19854  cmpsublem  19899  bwthOLD  19911  comppfsc  20033  filufint  20421  flimopn  20476  flimrest  20484  alexsubALTlem3  20549  equivcfil  21738  dvfsumrlim3  22434  pntlem3  23794  nbcusgra  24463  cusgrasize2inds  24477  usgrasscusgra  24483  cyclnspth  24631  fargshiftf1  24637  fargshiftfva  24639  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  wlkiswwlk1  24690  clwwlkgt0  24771  clwlkisclwwlklem2a  24785  erclwwlktr  24815  erclwwlkntr  24827  el2wlkonot  24869  el2spthonot  24870  usg2wlkonot  24883  usg2wotspth  24884  rusgrasn  24945  eupatrl  24968  frgraunss  24995  3cyclfrgrarn1  25012  3cyclfrgrarn  25013  vdfrgra0  25022  vdgn0frgrav2  25024  vdgn1frgrav2  25026  frgrancvvdeqlemB  25038  frgrawopreglem2  25045  frgrawopreglem5  25048  usg2spot2nb  25065  numclwwlkovf2ex  25086  frgrareggt1  25116  frgrareg  25117  frgraregord013  25118  grpoinveu  25224  rngoueqz  25432  zerdivemp1  25436  elspansn4  26491  atomli  27301  mdsymlem3  27324  mdsymlem5  27326  predpo  29264  nn0prpwlem  30140  rngonegrmul  30355  zerdivemp1x  30358  ssfz12  32330  usgra2pthspth  32351  initoeu1  32617  initoeu2lem1  32620  initoeu2  32622  termoeu1  32624  nzerooringczr  32880  lindslinindsimp1  33058  com3rgbi  33284  lshpdisj  34712  linepsubN  35476  pmapsub  35492  paddasslem5  35548  dalaw  35610  pclclN  35615  pclfinN  35624  trlval2  35888  tendospcanN  36750  diaintclN  36785  dibintclN  36894  dihintcl  37071  dvh4dimlem  37170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator