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

Step	Hyp	Ref	Expression
1		com4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	com4t 93	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com13 88	1 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜓 → 𝜏))))

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  propeqop  5526  po2ne  5624  fveqdmss  7112  tfrlem9  8441  omordi  8622  nnmordi  8687  fundmen  9096  pssnn  9234  fiint  9394  fiintOLD  9395  infssuni  9414  cfcoflem  10341  fin1a2lem10  10478  axdc3lem2  10520  zorn2lem7  10571  fpwwe2lem11  10710  genpnnp  11074  mulgt0sr  11174  nn01to3  13006  elfzodifsumelfzo  13782  ssfzo12  13809  elfznelfzo  13822  injresinjlem  13837  injresinj  13838  ssnn0fi  14036  expcan  14219  ltexp2  14220  hashgt12el2  14472  fi1uzind  14556  swrdswrdlem  14752  swrdswrd  14753  wrd2ind  14771  swrdccatin1  14773  cshwlen  14847  2cshwcshw  14874  cshwcsh2id  14877  dvdsmodexp  16310  dvdsaddre2b  16355  lcmfunsnlem2lem1  16685  lcmfdvdsb  16690  coprmproddvdslem  16709  infpnlem1  16957  cshwshashlem1  17143  initoeu1  18078  initoeu2lem1  18081  initoeu2  18083  termoeu1  18085  grpinveu  19014  mulgass2  20332  lss1d  20984  nzerooringczr  21514  cply1mul  22321  gsummoncoe1  22333  mp2pm2mplem4  22836  chpscmat  22869  chcoeffeq  22913  cnpnei  23293  hausnei2  23382  cmpsublem  23428  comppfsc  23561  filufint  23949  flimopn  24004  flimrest  24012  alexsubALTlem3  24078  equivcfil  25352  dvfsumrlim3  26094  pntlem3  27671  elntg2  29018  numedglnl  29179  cusgrsize2inds  29489  2pthnloop  29767  usgr2wlkneq  29792  elwspths2on  29993  clwwlkccatlem  30021  clwlkclwwlklem2a  30030  clwwisshclwws  30047  erclwwlktr  30054  erclwwlkntr  30103  3cyclfrgrrn1  30317  vdgn1frgrv2  30328  frgrncvvdeqlem8  30338  frgrwopreglem5  30353  frgrwopreglem5ALT  30354  frgr2wwlkeqm  30363  2clwwlk2clwwlk  30382  frgrregord013  30427  grpoinveu  30551  elspansn4  31605  atomli  32414  mdsymlem3  32437  mdsymlem5  32439  sat1el2xp  35347  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  nn0prpwlem  36288  axc11n11r  36649  broucube  37614  rngoueqz  37900  rngonegrmul  37904  zerdivemp1x  37907  lshpdisj  38943  linepsubN  39709  pmapsub  39725  paddasslem5  39781  dalaw  39843  pclclN  39848  pclfinN  39857  trlval2  40120  tendospcanN  40980  diaintclN  41015  dibintclN  41124  dihintcl  41301  dvh4dimlem  41400  com3rgbi  44485  2reu8i  47028  ssfz12  47229  iccpartlt  47298  iccelpart  47307  iccpartnel  47312  fargshiftf1  47315  fargshiftfva  47317  sbcpr  47395  reuopreuprim  47400  lighneallem3  47481  lighneal  47485  sbgoldbwt  47651  isuspgrimlem  47758  grimcnv  47763  grimco  47764  uhgrimisgrgriclem  47782  grimedg  47787  grlicsym  47830  lindslinindsimp1  48186