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  5455  po2ne  5549  fveqdmss  7026  resf1extb  7881  tfrlem9  8321  omordi  8498  nnmordi  8564  fundmen  8975  pssnn  9100  fiint  9234  infssuni  9253  cfcoflem  10192  fin1a2lem10  10329  axdc3lem2  10371  zorn2lem7  10422  fpwwe2lem11  10562  genpnnp  10926  mulgt0sr  11026  nn01to3  12889  fzdif1  13557  elfzodifsumelfzo  13684  ssfzo12  13712  elfznelfzo  13726  injresinjlem  13743  injresinj  13744  ssnn0fi  13945  expcan  14129  ltexp2  14130  hashgt12el2  14383  fi1uzind  14467  swrdswrdlem  14664  swrdswrd  14665  wrd2ind  14683  swrdccatin1  14685  cshwlen  14759  2cshwcshw  14785  cshwcsh2id  14788  dvdsmodexp  16227  dvdsaddre2b  16274  lcmfunsnlem2lem1  16605  lcmfdvdsb  16610  coprmproddvdslem  16629  infpnlem1  16879  cshwshashlem1  17064  initoeu1  17976  initoeu2lem1  17979  initoeu2  17981  termoeu1  17983  grpinveu  18948  mulgass2  20288  lss1d  20960  nzerooringczr  21462  cply1mul  22289  gsummoncoe1  22301  mp2pm2mplem4  22799  chpscmat  22832  chcoeffeq  22876  cnpnei  23254  hausnei2  23343  cmpsublem  23389  comppfsc  23522  filufint  23910  flimopn  23965  flimrest  23973  alexsubALTlem3  24039  equivcfil  25291  dvfsumrlim3  26025  pntlem3  27597  elntg2  29079  numedglnl  29238  cusgrsize2inds  29547  2pthnloop  29824  usgr2wlkneq  29849  elwspths2on  30055  elwspths2onw  30056  clwwlkccatlem  30084  clwlkclwwlklem2a  30093  clwwisshclwws  30110  erclwwlktr  30117  erclwwlkntr  30166  3cyclfrgrrn1  30380  vdgn1frgrv2  30391  frgrncvvdeqlem8  30401  frgrwopreglem5  30416  frgrwopreglem5ALT  30417  frgr2wwlkeqm  30426  2clwwlk2clwwlk  30445  frgrregord013  30490  grpoinveu  30615  elspansn4  31669  atomli  32478  mdsymlem3  32501  mdsymlem5  32503  sat1el2xp  35614  satffunlem  35636  satffunlem1lem1  35637  satffunlem2lem1  35639  nn0prpwlem  36557  axc11n11r  37033  broucube  38028  rngoueqz  38314  rngonegrmul  38318  zerdivemp1x  38321  lshpdisj  39486  linepsubN  40251  pmapsub  40267  paddasslem5  40323  dalaw  40385  pclclN  40390  pclfinN  40399  trlval2  40662  tendospcanN  41522  diaintclN  41557  dibintclN  41666  dihintcl  41843  dvh4dimlem  41942  com3rgbi  44965  2reu8i  47583  ssfz12  47784  iccpartlt  47906  iccelpart  47915  iccpartnel  47920  fargshiftf1  47923  fargshiftfva  47925  sbcpr  48003  reuopreuprim  48008  lighneallem3  48092  lighneal  48096  sbgoldbwt  48275  grimcnv  48386  grimco  48387  isuspgrimlem  48393  uhgrimisgrgriclem  48428  grimedg  48433  cycl3grtri  48445  isubgr3stgrlem6  48469  grlicsym  48511  clnbgr3stgrgrlic  48518  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem6  48622  lindslinindsimp1  48955