Theorem com24 96

Description: Commutation of antecedents. Swap 2nd and 4th. Deduction associated with com13 89. (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 94	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com13 89	1 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜓 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com25  100  propeqop  5492  po2ne  5587  fveqdmss  7077  resf1extb  7933  tfrlem9  8374  omordi  8553  nnmordi  8619  fundmen  9031  pssnn  9156  fiint  9289  infssuni  9306  cfcoflem  10267  fin1a2lem10  10404  axdc3lem2  10446  zorn2lem7  10497  fpwwe2lem11  10637  genpnnp  11001  mulgt0sr  11101  nn01to3  12976  fzdif1  13645  elfzodifsumelfzo  13772  ssfzo12  13800  elfznelfzo  13814  injresinjlem  13831  injresinj  13832  ssnn0fi  14034  expcan  14218  ltexp2  14219  hashgt12el2  14473  fi1uzind  14557  swrdswrdlem  14758  swrdswrd  14759  wrd2ind  14777  swrdccatin1  14779  cshwlen  14855  2cshwcshw  14881  cshwcsh2id  14884  dvdsmodexp  16335  dvdsaddre2b  16382  lcmfunsnlem2lem1  16713  lcmfdvdsb  16718  coprmproddvdslem  16737  infpnlem1  16987  cshwshashlem1  17172  initoeu1  18085  initoeu2lem1  18088  initoeu2  18090  termoeu1  18092  grpinveu  19064  mulgass2  20417  lss1d  21113  nzerooringczr  21659  cply1mul  22485  gsummoncoe1  22497  mp2pm2mplem4  22995  chpscmat  23028  chcoeffeq  23072  cnpnei  23450  hausnei2  23539  cmpsublem  23585  comppfsc  23718  filufint  24106  flimopn  24161  flimrest  24169  alexsubALTlem3  24235  equivcfil  25487  dvfsumrlim3  26221  pntlem3  27802  elntg2  29364  numedglnl  29523  cusgrsize2inds  29832  2pthnloop  30109  usgr2wlkneq  30134  elwspths2on  30340  elwspths2onw  30341  clwwlkccatlem  30369  clwlkclwwlklem2a  30378  clwwisshclwws  30395  erclwwlktr  30402  erclwwlkntr  30451  3cyclfrgrrn1  30665  vdgn1frgrv2  30676  frgrncvvdeqlem8  30686  frgrwopreglem5  30701  frgrwopreglem5ALT  30702  frgr2wwlkeqm  30711  2clwwlk2clwwlk  30730  frgrregord013  30775  grpoinveu  30900  elspansn4  31954  atomli  32763  mdsymlem3  32786  mdsymlem5  32788  sat1el2xp  35884  satffunlem  35906  satffunlem1lem1  35907  satffunlem2lem1  35909  nn0prpwlem  36866  axc11n11r  37341  broucube  38338  rngoueqz  38624  rngonegrmul  38628  zerdivemp1x  38631  lshpdisj  39794  linepsubN  40559  pmapsub  40575  paddasslem5  40631  dalaw  40693  pclclN  40698  pclfinN  40707  trlval2  40970  tendospcanN  41830  diaintclN  41865  dibintclN  41974  dihintcl  42151  dvh4dimlem  42250  com3rgbi  45256  2reu8i  47883  ssfz12  48084  iccpartlt  48206  iccelpart  48215  iccpartnel  48220  fargshiftf1  48223  fargshiftfva  48225  sbcpr  48303  reuopreuprim  48308  lighneallem3  48392  lighneal  48396  sbgoldbwt  48575  grimcnv  48686  grimco  48687  isuspgrimlem  48693  uhgrimisgrgriclem  48728  grimedg  48733  cycl3grtri  48745  isubgr3stgrlem6  48769  grlicsym  48811  clnbgr3stgrgrlic  48818  pgnbgreunbgrlem3  48916  pgnbgreunbgrlem6  48922  lindslinindsimp1  49270