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  5566  fveqdmss  7034  tfrlem9  8336  omordi  8518  nnmordi  8583  fundmen  8982  pssnn  9119  pssnnOLD  9216  fiint  9275  infssuni  9294  cfcoflem  10217  fin1a2lem10  10354  axdc3lem2  10396  zorn2lem7  10447  fpwwe2lem11  10586  genpnnp  10950  mulgt0sr  11050  nn01to3  12875  elfzodifsumelfzo  13648  ssfzo12  13675  elfznelfzo  13687  injresinjlem  13702  injresinj  13703  ssnn0fi  13900  expcan  14084  ltexp2  14085  hashgt12el2  14333  fi1uzind  14408  swrdswrdlem  14604  swrdswrd  14605  wrd2ind  14623  swrdccatin1  14625  cshwlen  14699  2cshwcshw  14726  cshwcsh2id  14729  dvdsmodexp  16155  dvdsaddre2b  16200  lcmfunsnlem2lem1  16525  lcmfdvdsb  16530  coprmproddvdslem  16549  infpnlem1  16793  cshwshashlem1  16979  initoeu1  17911  initoeu2lem1  17914  initoeu2  17916  termoeu1  17918  grpinveu  18799  mulgass2  20039  lss1d  20481  cply1mul  21702  gsummoncoe1  21712  mp2pm2mplem4  22195  chpscmat  22228  chcoeffeq  22272  cnpnei  22652  hausnei2  22741  cmpsublem  22787  comppfsc  22920  filufint  23308  flimopn  23363  flimrest  23371  alexsubALTlem3  23437  equivcfil  24700  dvfsumrlim3  25434  pntlem3  26994  elntg2  27997  numedglnl  28158  cusgrsize2inds  28464  2pthnloop  28742  usgr2wlkneq  28767  elwspths2on  28968  clwwlkccatlem  28996  clwlkclwwlklem2a  29005  clwwisshclwws  29022  erclwwlktr  29029  erclwwlkntr  29078  3cyclfrgrrn1  29292  vdgn1frgrv2  29303  frgrncvvdeqlem8  29313  frgrwopreglem5  29328  frgrwopreglem5ALT  29329  frgr2wwlkeqm  29338  2clwwlk2clwwlk  29357  frgrregord013  29402  grpoinveu  29524  elspansn4  30578  atomli  31387  mdsymlem3  31410  mdsymlem5  31412  sat1el2xp  34060  satffunlem  34082  satffunlem1lem1  34083  satffunlem2lem1  34085  nn0prpwlem  34870  axc11n11r  35224  broucube  36185  rngoueqz  36472  rngonegrmul  36476  zerdivemp1x  36479  lshpdisj  37522  linepsubN  38288  pmapsub  38304  paddasslem5  38360  dalaw  38422  pclclN  38427  pclfinN  38436  trlval2  38699  tendospcanN  39559  diaintclN  39594  dibintclN  39703  dihintcl  39880  dvh4dimlem  39979  com3rgbi  42918  2reu8i  45465  ssfz12  45666  iccpartlt  45736  iccelpart  45745  iccpartnel  45750  fargshiftf1  45753  fargshiftfva  45755  sbcpr  45833  reuopreuprim  45838  lighneallem3  45919  lighneal  45923  sbgoldbwt  46089  isomuspgrlem2b  46141  nzerooringczr  46490  lindslinindsimp1  46658