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  5469  po2ne  5564  fveqdmss  7052  resf1extb  7912  tfrlem9  8355  omordi  8532  nnmordi  8597  fundmen  9004  pssnn  9137  fiint  9283  fiintOLD  9284  infssuni  9303  cfcoflem  10231  fin1a2lem10  10368  axdc3lem2  10410  zorn2lem7  10461  fpwwe2lem11  10600  genpnnp  10964  mulgt0sr  11064  nn01to3  12906  fzdif1  13572  elfzodifsumelfzo  13698  ssfzo12  13726  elfznelfzo  13739  injresinjlem  13754  injresinj  13755  ssnn0fi  13956  expcan  14140  ltexp2  14141  hashgt12el2  14394  fi1uzind  14478  swrdswrdlem  14675  swrdswrd  14676  wrd2ind  14694  swrdccatin1  14696  cshwlen  14770  2cshwcshw  14797  cshwcsh2id  14800  dvdsmodexp  16236  dvdsaddre2b  16283  lcmfunsnlem2lem1  16614  lcmfdvdsb  16619  coprmproddvdslem  16638  infpnlem1  16887  cshwshashlem1  17072  initoeu1  17979  initoeu2lem1  17982  initoeu2  17984  termoeu1  17986  grpinveu  18912  mulgass2  20224  lss1d  20875  nzerooringczr  21396  cply1mul  22189  gsummoncoe1  22201  mp2pm2mplem4  22702  chpscmat  22735  chcoeffeq  22779  cnpnei  23157  hausnei2  23246  cmpsublem  23292  comppfsc  23425  filufint  23813  flimopn  23868  flimrest  23876  alexsubALTlem3  23942  equivcfil  25205  dvfsumrlim3  25946  pntlem3  27526  elntg2  28918  numedglnl  29077  cusgrsize2inds  29387  2pthnloop  29667  usgr2wlkneq  29692  elwspths2on  29896  clwwlkccatlem  29924  clwlkclwwlklem2a  29933  clwwisshclwws  29950  erclwwlktr  29957  erclwwlkntr  30006  3cyclfrgrrn1  30220  vdgn1frgrv2  30231  frgrncvvdeqlem8  30241  frgrwopreglem5  30256  frgrwopreglem5ALT  30257  frgr2wwlkeqm  30266  2clwwlk2clwwlk  30285  frgrregord013  30330  grpoinveu  30454  elspansn4  31508  atomli  32317  mdsymlem3  32340  mdsymlem5  32342  sat1el2xp  35366  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  nn0prpwlem  36305  axc11n11r  36666  broucube  37643  rngoueqz  37929  rngonegrmul  37933  zerdivemp1x  37936  lshpdisj  38975  linepsubN  39741  pmapsub  39757  paddasslem5  39813  dalaw  39875  pclclN  39880  pclfinN  39889  trlval2  40152  tendospcanN  41012  diaintclN  41047  dibintclN  41156  dihintcl  41333  dvh4dimlem  41432  com3rgbi  44497  2reu8i  47104  ssfz12  47305  iccpartlt  47415  iccelpart  47424  iccpartnel  47429  fargshiftf1  47432  fargshiftfva  47434  sbcpr  47512  reuopreuprim  47517  lighneallem3  47598  lighneal  47602  sbgoldbwt  47768  grimcnv  47878  grimco  47879  isuspgrimlem  47885  uhgrimisgrgriclem  47920  grimedg  47925  cycl3grtri  47936  isubgr3stgrlem6  47960  grlicsym  47995  clnbgr3stgrgrlic  48001  pgnbgreunbgrlem3  48098  pgnbgreunbgrlem6  48104  lindslinindsimp1  48436