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

Theorem com24 95
 Description: Commutation of antecedents. Swap 2nd and 4th. Deduction associated with com13 88. (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 93 . 2 (𝜒 → (𝜃 → (𝜑 → (𝜓𝜏))))
32com13 88 1 (𝜑 → (𝜃 → (𝜒 → (𝜓𝜏))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7 This theorem is referenced by:  com25  99  imim12  105  propeqop  5118  predpo  5859  fveqdmss  6517  tfrlem9  7650  omordi  7815  nnmordi  7880  fundmen  8195  pssnn  8343  fiint  8402  infssuni  8422  cfcoflem  9286  fin1a2lem10  9423  axdc3lem2  9465  zorn2lem7  9516  fpwwe2lem12  9655  genpnnp  10019  mulgt0sr  10118  nn01to3  11974  elfzodifsumelfzo  12728  ssfzo12  12755  elfznelfzo  12767  injresinjlem  12782  injresinj  12783  ssnn0fi  12978  expcan  13107  ltexp2  13108  hashgt12el2  13403  fi1uzind  13471  swrdswrdlem  13659  swrdswrd  13660  wrd2ind  13677  swrdccatin1  13683  cshwlen  13745  2cshwcshw  13771  cshwcsh2id  13774  dvdsmodexp  15190  dvdsaddre2b  15231  lcmfunsnlem2lem1  15553  lcmfdvdsb  15558  coprmproddvdslem  15578  infpnlem1  15816  cshwshashlem1  16004  initoeu1  16862  initoeu2lem1  16865  initoeu2  16867  termoeu1  16869  grpinveu  17657  mulgass2  18801  lss1d  19165  cply1mul  19866  gsummoncoe1  19876  mp2pm2mplem4  20816  chpscmat  20849  chcoeffeq  20893  cnpnei  21270  hausnei2  21359  cmpsublem  21404  comppfsc  21537  filufint  21925  flimopn  21980  flimrest  21988  alexsubALTlem3  22054  equivcfil  23297  dvfsumrlim3  23995  pntlem3  25497  numedglnl  26238  cusgrsize2inds  26559  2pthnloop  26837  usgr2wlkneq  26862  elwspths2on  27081  clwwlkccatlem  27112  clwlkclwwlklem2a  27121  clwwisshclwws  27138  erclwwlktr  27145  erclwwlkntr  27202  clwlksfclwwlkOLD  27216  3cyclfrgrrn1  27439  vdgn1frgrv2  27450  frgrncvvdeqlem8  27460  frgrwopreglem5  27475  frgrwopreglem5ALT  27476  frgr2wwlkeqm  27485  2clwwlk2clwwlk  27507  frgrregord013  27563  grpoinveu  27682  elspansn4  28741  atomli  29550  mdsymlem3  29573  mdsymlem5  29575  nn0prpwlem  32623  axc11n11r  32979  broucube  33756  rngoueqz  34052  rngonegrmul  34056  zerdivemp1x  34059  lshpdisj  34777  linepsubN  35541  pmapsub  35557  paddasslem5  35613  dalaw  35675  pclclN  35680  pclfinN  35689  trlval2  35953  tendospcanN  36814  diaintclN  36849  dibintclN  36958  dihintcl  37135  dvh4dimlem  37234  com3rgbi  39222  ssfz12  41834  iccpartlt  41870  iccelpart  41879  iccpartnel  41884  fargshiftf1  41887  fargshiftfva  41889  lighneallem3  42034  lighneal  42038  sbgoldbwt  42175  nzerooringczr  42582  lindslinindsimp1  42756
 Copyright terms: Public domain W3C validator