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  5548  fveqdmss  7023  resf1extb  7876  tfrlem9  8316  omordi  8493  nnmordi  8559  fundmen  8968  pssnn  9093  fiint  9227  infssuni  9246  cfcoflem  10182  fin1a2lem10  10319  axdc3lem2  10361  zorn2lem7  10412  fpwwe2lem11  10552  genpnnp  10916  mulgt0sr  11016  nn01to3  12854  fzdif1  13521  elfzodifsumelfzo  13647  ssfzo12  13675  elfznelfzo  13689  injresinjlem  13706  injresinj  13707  ssnn0fi  13908  expcan  14092  ltexp2  14093  hashgt12el2  14346  fi1uzind  14430  swrdswrdlem  14627  swrdswrd  14628  wrd2ind  14646  swrdccatin1  14648  cshwlen  14722  2cshwcshw  14748  cshwcsh2id  14751  dvdsmodexp  16187  dvdsaddre2b  16234  lcmfunsnlem2lem1  16565  lcmfdvdsb  16570  coprmproddvdslem  16589  infpnlem1  16838  cshwshashlem1  17023  initoeu1  17935  initoeu2lem1  17938  initoeu2  17940  termoeu1  17942  grpinveu  18904  mulgass2  20244  lss1d  20914  nzerooringczr  21435  cply1mul  22240  gsummoncoe1  22252  mp2pm2mplem4  22753  chpscmat  22786  chcoeffeq  22830  cnpnei  23208  hausnei2  23297  cmpsublem  23343  comppfsc  23476  filufint  23864  flimopn  23919  flimrest  23927  alexsubALTlem3  23993  equivcfil  25255  dvfsumrlim3  25996  pntlem3  27576  elntg2  29058  numedglnl  29217  cusgrsize2inds  29527  2pthnloop  29804  usgr2wlkneq  29829  elwspths2on  30035  elwspths2onw  30036  clwwlkccatlem  30064  clwlkclwwlklem2a  30073  clwwisshclwws  30090  erclwwlktr  30097  erclwwlkntr  30146  3cyclfrgrrn1  30360  vdgn1frgrv2  30371  frgrncvvdeqlem8  30381  frgrwopreglem5  30396  frgrwopreglem5ALT  30397  frgr2wwlkeqm  30406  2clwwlk2clwwlk  30425  frgrregord013  30470  grpoinveu  30594  elspansn4  31648  atomli  32457  mdsymlem3  32480  mdsymlem5  32482  sat1el2xp  35573  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  nn0prpwlem  36516  axc11n11r  36884  broucube  37855  rngoueqz  38141  rngonegrmul  38145  zerdivemp1x  38148  lshpdisj  39247  linepsubN  40012  pmapsub  40028  paddasslem5  40084  dalaw  40146  pclclN  40151  pclfinN  40160  trlval2  40423  tendospcanN  41283  diaintclN  41318  dibintclN  41427  dihintcl  41604  dvh4dimlem  41703  com3rgbi  44755  2reu8i  47359  ssfz12  47560  iccpartlt  47670  iccelpart  47679  iccpartnel  47684  fargshiftf1  47687  fargshiftfva  47689  sbcpr  47767  reuopreuprim  47772  lighneallem3  47853  lighneal  47857  sbgoldbwt  48023  grimcnv  48134  grimco  48135  isuspgrimlem  48141  uhgrimisgrgriclem  48176  grimedg  48181  cycl3grtri  48193  isubgr3stgrlem6  48217  grlicsym  48259  clnbgr3stgrgrlic  48266  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370  lindslinindsimp1  48703