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  5512  po2ne  5608  fveqdmss  7098  resf1extb  7956  tfrlem9  8425  omordi  8604  nnmordi  8669  fundmen  9071  pssnn  9208  fiint  9366  fiintOLD  9367  infssuni  9386  cfcoflem  10312  fin1a2lem10  10449  axdc3lem2  10491  zorn2lem7  10542  fpwwe2lem11  10681  genpnnp  11045  mulgt0sr  11145  nn01to3  12983  fzdif1  13645  elfzodifsumelfzo  13770  ssfzo12  13798  elfznelfzo  13811  injresinjlem  13826  injresinj  13827  ssnn0fi  14026  expcan  14209  ltexp2  14210  hashgt12el2  14462  fi1uzind  14546  swrdswrdlem  14742  swrdswrd  14743  wrd2ind  14761  swrdccatin1  14763  cshwlen  14837  2cshwcshw  14864  cshwcsh2id  14867  dvdsmodexp  16298  dvdsaddre2b  16344  lcmfunsnlem2lem1  16675  lcmfdvdsb  16680  coprmproddvdslem  16699  infpnlem1  16948  cshwshashlem1  17133  initoeu1  18056  initoeu2lem1  18059  initoeu2  18061  termoeu1  18063  grpinveu  18992  mulgass2  20306  lss1d  20961  nzerooringczr  21491  cply1mul  22300  gsummoncoe1  22312  mp2pm2mplem4  22815  chpscmat  22848  chcoeffeq  22892  cnpnei  23272  hausnei2  23361  cmpsublem  23407  comppfsc  23540  filufint  23928  flimopn  23983  flimrest  23991  alexsubALTlem3  24057  equivcfil  25333  dvfsumrlim3  26074  pntlem3  27653  elntg2  29000  numedglnl  29161  cusgrsize2inds  29471  2pthnloop  29751  usgr2wlkneq  29776  elwspths2on  29980  clwwlkccatlem  30008  clwlkclwwlklem2a  30017  clwwisshclwws  30034  erclwwlktr  30041  erclwwlkntr  30090  3cyclfrgrrn1  30304  vdgn1frgrv2  30315  frgrncvvdeqlem8  30325  frgrwopreglem5  30340  frgrwopreglem5ALT  30341  frgr2wwlkeqm  30350  2clwwlk2clwwlk  30369  frgrregord013  30414  grpoinveu  30538  elspansn4  31592  atomli  32401  mdsymlem3  32424  mdsymlem5  32426  sat1el2xp  35384  satffunlem  35406  satffunlem1lem1  35407  satffunlem2lem1  35409  nn0prpwlem  36323  axc11n11r  36684  broucube  37661  rngoueqz  37947  rngonegrmul  37951  zerdivemp1x  37954  lshpdisj  38988  linepsubN  39754  pmapsub  39770  paddasslem5  39826  dalaw  39888  pclclN  39893  pclfinN  39902  trlval2  40165  tendospcanN  41025  diaintclN  41060  dibintclN  41169  dihintcl  41346  dvh4dimlem  41445  com3rgbi  44534  2reu8i  47125  ssfz12  47326  iccpartlt  47411  iccelpart  47420  iccpartnel  47425  fargshiftf1  47428  fargshiftfva  47430  sbcpr  47508  reuopreuprim  47513  lighneallem3  47594  lighneal  47598  sbgoldbwt  47764  isuspgrimlem  47874  grimcnv  47879  grimco  47880  uhgrimisgrgriclem  47898  grimedg  47903  cycl3grtri  47914  isubgr3stgrlem6  47938  grlicsym  47973  clnbgr3stgrgrlic  47979  lindslinindsimp1  48374