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  5452  po2ne  5545  fveqdmss  7020  resf1extb  7873  tfrlem9  8313  omordi  8490  nnmordi  8555  fundmen  8964  pssnn  9089  fiint  9222  infssuni  9241  cfcoflem  10174  fin1a2lem10  10311  axdc3lem2  10353  zorn2lem7  10404  fpwwe2lem11  10543  genpnnp  10907  mulgt0sr  11007  nn01to3  12845  fzdif1  13512  elfzodifsumelfzo  13638  ssfzo12  13666  elfznelfzo  13680  injresinjlem  13697  injresinj  13698  ssnn0fi  13899  expcan  14083  ltexp2  14084  hashgt12el2  14337  fi1uzind  14421  swrdswrdlem  14618  swrdswrd  14619  wrd2ind  14637  swrdccatin1  14639  cshwlen  14713  2cshwcshw  14739  cshwcsh2id  14742  dvdsmodexp  16178  dvdsaddre2b  16225  lcmfunsnlem2lem1  16556  lcmfdvdsb  16561  coprmproddvdslem  16580  infpnlem1  16829  cshwshashlem1  17014  initoeu1  17926  initoeu2lem1  17929  initoeu2  17931  termoeu1  17933  grpinveu  18895  mulgass2  20235  lss1d  20905  nzerooringczr  21426  cply1mul  22231  gsummoncoe1  22243  mp2pm2mplem4  22744  chpscmat  22777  chcoeffeq  22821  cnpnei  23199  hausnei2  23288  cmpsublem  23334  comppfsc  23467  filufint  23855  flimopn  23910  flimrest  23918  alexsubALTlem3  23984  equivcfil  25246  dvfsumrlim3  25987  pntlem3  27567  elntg2  28984  numedglnl  29143  cusgrsize2inds  29453  2pthnloop  29730  usgr2wlkneq  29755  elwspths2on  29961  elwspths2onw  29962  clwwlkccatlem  29990  clwlkclwwlklem2a  29999  clwwisshclwws  30016  erclwwlktr  30023  erclwwlkntr  30072  3cyclfrgrrn1  30286  vdgn1frgrv2  30297  frgrncvvdeqlem8  30307  frgrwopreglem5  30322  frgrwopreglem5ALT  30323  frgr2wwlkeqm  30332  2clwwlk2clwwlk  30351  frgrregord013  30396  grpoinveu  30520  elspansn4  31574  atomli  32383  mdsymlem3  32406  mdsymlem5  32408  sat1el2xp  35495  satffunlem  35517  satffunlem1lem1  35518  satffunlem2lem1  35520  nn0prpwlem  36438  axc11n11r  36800  broucube  37767  rngoueqz  38053  rngonegrmul  38057  zerdivemp1x  38060  lshpdisj  39159  linepsubN  39924  pmapsub  39940  paddasslem5  39996  dalaw  40058  pclclN  40063  pclfinN  40072  trlval2  40335  tendospcanN  41195  diaintclN  41230  dibintclN  41339  dihintcl  41516  dvh4dimlem  41615  com3rgbi  44671  2reu8i  47275  ssfz12  47476  iccpartlt  47586  iccelpart  47595  iccpartnel  47600  fargshiftf1  47603  fargshiftfva  47605  sbcpr  47683  reuopreuprim  47688  lighneallem3  47769  lighneal  47773  sbgoldbwt  47939  grimcnv  48050  grimco  48051  isuspgrimlem  48057  uhgrimisgrgriclem  48092  grimedg  48097  cycl3grtri  48109  isubgr3stgrlem6  48133  grlicsym  48175  clnbgr3stgrgrlic  48182  pgnbgreunbgrlem3  48280  pgnbgreunbgrlem6  48286  lindslinindsimp1  48619