MPE Home 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  4935  predpo  5662  fveqdmss  6315  tfrlem9  7433  omordi  7598  nnmordi  7663  fundmen  7982  pssnn  8130  fiint  8189  infssuni  8209  cfcoflem  9046  fin1a2lem10  9183  axdc3lem2  9225  zorn2lem7  9276  fpwwe2lem12  9415  genpnnp  9779  mulgt0sr  9878  nn01to3  11733  elfzodifsumelfzo  12482  ssfzo12  12510  elfznelfzo  12522  injresinjlem  12536  injresinj  12537  ssnn0fi  12732  expcan  12861  ltexp2  12862  hashgt12el2  13159  fi1uzind  13226  fi1uzindOLD  13232  swrdswrdlem  13405  swrdswrd  13406  wrd2ind  13423  swrdccatin1  13428  cshwlen  13490  2cshwcshw  13516  cshwcsh2id  13519  dvdsaddre2b  14964  lcmfunsnlem2lem1  15286  lcmfdvdsb  15291  coprmproddvdslem  15311  infpnlem1  15549  cshwshashlem1  15737  initoeu1  16593  initoeu2lem1  16596  initoeu2  16598  termoeu1  16600  grpinveu  17388  mulgass2  18533  lss1d  18895  cply1mul  19596  gsummoncoe1  19606  mp2pm2mplem4  20546  chpscmat  20579  chcoeffeq  20623  cnpnei  20991  hausnei2  21080  cmpsublem  21125  comppfsc  21258  filufint  21647  flimopn  21702  flimrest  21710  alexsubALTlem3  21776  equivcfil  23020  dvfsumrlim3  23717  pntlem3  25215  cusgrsize2inds  26253  2pthnloop  26513  usgr2wlkneq  26538  elwspths2on  26738  clwlkclwwlklem2a  26783  clwwisshclwws  26811  erclwwlkstr  26819  erclwwlksntr  26831  clwlksfclwwlk  26845  3cyclfrgrrn1  27030  vdgn1frgrv2  27041  frgrncvvdeqlemB  27052  frgrwopreglem5  27060  numclwwlkovf2ex  27092  frgrregord013  27124  grpoinveu  27243  elspansn4  28302  atomli  29111  mdsymlem3  29134  mdsymlem5  29136  nn0prpwlem  31994  axc11n11r  32350  broucube  33110  rngoueqz  33406  rngonegrmul  33410  zerdivemp1x  33413  lshpdisj  33789  linepsubN  34553  pmapsub  34569  paddasslem5  34625  dalaw  34687  pclclN  34692  pclfinN  34701  trlval2  34965  tendospcanN  35827  diaintclN  35862  dibintclN  35971  dihintcl  36148  dvh4dimlem  36247  com3rgbi  38237  ssfz12  40647  iccpartlt  40684  iccelpart  40693  iccpartnel  40698  fargshiftf1  40701  fargshiftfva  40703  lighneallem3  40849  lighneal  40853  bgoldbwt  40986  nzerooringczr  41386  lindslinindsimp1  41560
  Copyright terms: Public domain W3C validator