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  5423  po2ne  5518  fveqdmss  6950  tfrlem9  8200  omordi  8373  nnmordi  8438  fundmen  8791  pssnn  8916  pssnnOLD  9001  fiint  9052  infssuni  9071  cfcoflem  10012  fin1a2lem10  10149  axdc3lem2  10191  zorn2lem7  10242  fpwwe2lem11  10381  genpnnp  10745  mulgt0sr  10845  nn01to3  12663  elfzodifsumelfzo  13434  ssfzo12  13461  elfznelfzo  13473  injresinjlem  13488  injresinj  13489  ssnn0fi  13686  expcan  13868  ltexp2  13869  hashgt12el2  14119  fi1uzind  14192  swrdswrdlem  14398  swrdswrd  14399  wrd2ind  14417  swrdccatin1  14419  cshwlen  14493  2cshwcshw  14519  cshwcsh2id  14522  dvdsmodexp  15952  dvdsaddre2b  15997  lcmfunsnlem2lem1  16324  lcmfdvdsb  16329  coprmproddvdslem  16348  infpnlem1  16592  cshwshashlem1  16778  initoeu1  17707  initoeu2lem1  17710  initoeu2  17712  termoeu1  17714  grpinveu  18595  mulgass2  19821  lss1d  20206  cply1mul  21446  gsummoncoe1  21456  mp2pm2mplem4  21939  chpscmat  21972  chcoeffeq  22016  cnpnei  22396  hausnei2  22485  cmpsublem  22531  comppfsc  22664  filufint  23052  flimopn  23107  flimrest  23115  alexsubALTlem3  23181  equivcfil  24444  dvfsumrlim3  25178  pntlem3  26738  elntg2  27334  numedglnl  27495  cusgrsize2inds  27801  2pthnloop  28078  usgr2wlkneq  28103  elwspths2on  28304  clwwlkccatlem  28332  clwlkclwwlklem2a  28341  clwwisshclwws  28358  erclwwlktr  28365  erclwwlkntr  28414  3cyclfrgrrn1  28628  vdgn1frgrv2  28639  frgrncvvdeqlem8  28649  frgrwopreglem5  28664  frgrwopreglem5ALT  28665  frgr2wwlkeqm  28674  2clwwlk2clwwlk  28693  frgrregord013  28738  grpoinveu  28860  elspansn4  29914  atomli  30723  mdsymlem3  30746  mdsymlem5  30748  sat1el2xp  33320  satffunlem  33342  satffunlem1lem1  33343  satffunlem2lem1  33345  nn0prpwlem  34490  axc11n11r  34844  broucube  35790  rngoueqz  36077  rngonegrmul  36081  zerdivemp1x  36084  lshpdisj  36980  linepsubN  37745  pmapsub  37761  paddasslem5  37817  dalaw  37879  pclclN  37884  pclfinN  37893  trlval2  38156  tendospcanN  39016  diaintclN  39051  dibintclN  39160  dihintcl  39337  dvh4dimlem  39436  com3rgbi  42087  2reu8i  44556  ssfz12  44758  iccpartlt  44828  iccelpart  44837  iccpartnel  44842  fargshiftf1  44845  fargshiftfva  44847  sbcpr  44925  reuopreuprim  44930  lighneallem3  45011  lighneal  45015  sbgoldbwt  45181  isomuspgrlem2b  45233  nzerooringczr  45582  lindslinindsimp1  45750