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  5462  po2ne  5555  fveqdmss  7032  resf1extb  7890  tfrlem9  8330  omordi  8507  nnmordi  8572  fundmen  8979  pssnn  9109  fiint  9253  fiintOLD  9254  infssuni  9273  cfcoflem  10201  fin1a2lem10  10338  axdc3lem2  10380  zorn2lem7  10431  fpwwe2lem11  10570  genpnnp  10934  mulgt0sr  11034  nn01to3  12876  fzdif1  13542  elfzodifsumelfzo  13668  ssfzo12  13696  elfznelfzo  13709  injresinjlem  13724  injresinj  13725  ssnn0fi  13926  expcan  14110  ltexp2  14111  hashgt12el2  14364  fi1uzind  14448  swrdswrdlem  14645  swrdswrd  14646  wrd2ind  14664  swrdccatin1  14666  cshwlen  14740  2cshwcshw  14767  cshwcsh2id  14770  dvdsmodexp  16206  dvdsaddre2b  16253  lcmfunsnlem2lem1  16584  lcmfdvdsb  16589  coprmproddvdslem  16608  infpnlem1  16857  cshwshashlem1  17042  initoeu1  17949  initoeu2lem1  17952  initoeu2  17954  termoeu1  17956  grpinveu  18882  mulgass2  20194  lss1d  20845  nzerooringczr  21366  cply1mul  22159  gsummoncoe1  22171  mp2pm2mplem4  22672  chpscmat  22705  chcoeffeq  22749  cnpnei  23127  hausnei2  23216  cmpsublem  23262  comppfsc  23395  filufint  23783  flimopn  23838  flimrest  23846  alexsubALTlem3  23912  equivcfil  25175  dvfsumrlim3  25916  pntlem3  27496  elntg2  28888  numedglnl  29047  cusgrsize2inds  29357  2pthnloop  29634  usgr2wlkneq  29659  elwspths2on  29863  clwwlkccatlem  29891  clwlkclwwlklem2a  29900  clwwisshclwws  29917  erclwwlktr  29924  erclwwlkntr  29973  3cyclfrgrrn1  30187  vdgn1frgrv2  30198  frgrncvvdeqlem8  30208  frgrwopreglem5  30223  frgrwopreglem5ALT  30224  frgr2wwlkeqm  30233  2clwwlk2clwwlk  30252  frgrregord013  30297  grpoinveu  30421  elspansn4  31475  atomli  32284  mdsymlem3  32307  mdsymlem5  32309  sat1el2xp  35339  satffunlem  35361  satffunlem1lem1  35362  satffunlem2lem1  35364  nn0prpwlem  36283  axc11n11r  36644  broucube  37621  rngoueqz  37907  rngonegrmul  37911  zerdivemp1x  37914  lshpdisj  38953  linepsubN  39719  pmapsub  39735  paddasslem5  39791  dalaw  39853  pclclN  39858  pclfinN  39867  trlval2  40130  tendospcanN  40990  diaintclN  41025  dibintclN  41134  dihintcl  41311  dvh4dimlem  41410  com3rgbi  44477  2reu8i  47087  ssfz12  47288  iccpartlt  47398  iccelpart  47407  iccpartnel  47412  fargshiftf1  47415  fargshiftfva  47417  sbcpr  47495  reuopreuprim  47500  lighneallem3  47581  lighneal  47585  sbgoldbwt  47751  grimcnv  47861  grimco  47862  isuspgrimlem  47868  uhgrimisgrgriclem  47903  grimedg  47908  cycl3grtri  47919  isubgr3stgrlem6  47943  grlicsym  47978  clnbgr3stgrgrlic  47984  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem6  48087  lindslinindsimp1  48419