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  5424  po2ne  5519  fveqdmss  6951  tfrlem9  8205  omordi  8380  nnmordi  8445  fundmen  8802  pssnn  8931  pssnnOLD  9016  fiint  9067  infssuni  9086  cfcoflem  10027  fin1a2lem10  10164  axdc3lem2  10206  zorn2lem7  10257  fpwwe2lem11  10396  genpnnp  10760  mulgt0sr  10860  nn01to3  12678  elfzodifsumelfzo  13449  ssfzo12  13476  elfznelfzo  13488  injresinjlem  13503  injresinj  13504  ssnn0fi  13701  expcan  13883  ltexp2  13884  hashgt12el2  14134  fi1uzind  14207  swrdswrdlem  14413  swrdswrd  14414  wrd2ind  14432  swrdccatin1  14434  cshwlen  14508  2cshwcshw  14534  cshwcsh2id  14537  dvdsmodexp  15967  dvdsaddre2b  16012  lcmfunsnlem2lem1  16339  lcmfdvdsb  16344  coprmproddvdslem  16363  infpnlem1  16607  cshwshashlem1  16793  initoeu1  17722  initoeu2lem1  17725  initoeu2  17727  termoeu1  17729  grpinveu  18610  mulgass2  19836  lss1d  20221  cply1mul  21461  gsummoncoe1  21471  mp2pm2mplem4  21954  chpscmat  21987  chcoeffeq  22031  cnpnei  22411  hausnei2  22500  cmpsublem  22546  comppfsc  22679  filufint  23067  flimopn  23122  flimrest  23130  alexsubALTlem3  23196  equivcfil  24459  dvfsumrlim3  25193  pntlem3  26753  elntg2  27349  numedglnl  27510  cusgrsize2inds  27816  2pthnloop  28093  usgr2wlkneq  28118  elwspths2on  28319  clwwlkccatlem  28347  clwlkclwwlklem2a  28356  clwwisshclwws  28373  erclwwlktr  28380  erclwwlkntr  28429  3cyclfrgrrn1  28643  vdgn1frgrv2  28654  frgrncvvdeqlem8  28664  frgrwopreglem5  28679  frgrwopreglem5ALT  28680  frgr2wwlkeqm  28689  2clwwlk2clwwlk  28708  frgrregord013  28753  grpoinveu  28875  elspansn4  29929  atomli  30738  mdsymlem3  30761  mdsymlem5  30763  sat1el2xp  33335  satffunlem  33357  satffunlem1lem1  33358  satffunlem2lem1  33360  nn0prpwlem  34505  axc11n11r  34859  broucube  35805  rngoueqz  36092  rngonegrmul  36096  zerdivemp1x  36099  lshpdisj  36995  linepsubN  37760  pmapsub  37776  paddasslem5  37832  dalaw  37894  pclclN  37899  pclfinN  37908  trlval2  38171  tendospcanN  39031  diaintclN  39066  dibintclN  39175  dihintcl  39352  dvh4dimlem  39451  com3rgbi  42102  2reu8i  44571  ssfz12  44773  iccpartlt  44843  iccelpart  44852  iccpartnel  44857  fargshiftf1  44860  fargshiftfva  44862  sbcpr  44940  reuopreuprim  44945  lighneallem3  45026  lighneal  45030  sbgoldbwt  45196  isomuspgrlem2b  45248  nzerooringczr  45597  lindslinindsimp1  45765