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  imim12  105  propeqop  5253  po2ne  5341  predpo  6004  fveqdmss  6671  tfrlem9  7825  omordi  7993  nnmordi  8058  fundmen  8380  pssnn  8531  fiint  8590  infssuni  8610  cfcoflem  9492  fin1a2lem10  9629  axdc3lem2  9671  zorn2lem7  9722  fpwwe2lem12  9861  genpnnp  10225  mulgt0sr  10325  nn01to3  12155  elfzodifsumelfzo  12918  ssfzo12  12945  elfznelfzo  12957  injresinjlem  12972  injresinj  12973  ssnn0fi  13168  expcan  13348  ltexp2  13349  hashgt12el2  13597  fi1uzind  13666  swrdswrdlem  13886  swrdswrd  13887  wrd2ind  13917  wrd2indOLD  13918  swrdccatin1  13924  cshwlen  14023  2cshwcshw  14049  cshwcsh2id  14052  dvdsmodexp  15475  dvdsaddre2b  15517  lcmfunsnlem2lem1  15838  lcmfdvdsb  15843  coprmproddvdslem  15862  infpnlem1  16102  cshwshashlem1  16285  initoeu1  17129  initoeu2lem1  17132  initoeu2  17134  termoeu1  17136  grpinveu  17925  mulgass2  19074  lss1d  19457  cply1mul  20165  gsummoncoe1  20175  mp2pm2mplem4  21121  chpscmat  21154  chcoeffeq  21198  cnpnei  21576  hausnei2  21665  cmpsublem  21711  comppfsc  21844  filufint  22232  flimopn  22287  flimrest  22295  alexsubALTlem3  22361  equivcfil  23605  dvfsumrlim3  24333  pntlem3  25887  elntg2  26474  numedglnl  26632  cusgrsize2inds  26938  2pthnloop  27220  usgr2wlkneq  27245  elwspths2on  27466  clwwlkccatlem  27495  clwlkclwwlklem2a  27504  clwwisshclwws  27530  erclwwlktr  27537  erclwwlkntr  27595  3cyclfrgrrn1  27819  vdgn1frgrv2  27830  frgrncvvdeqlem8  27840  frgrwopreglem5  27855  frgrwopreglem5ALT  27856  frgr2wwlkeqm  27865  2clwwlk2clwwlk  27887  2clwwlk2clwwlkOLD  27888  frgrregord013  27952  grpoinveu  28073  elspansn4  29131  atomli  29940  mdsymlem3  29963  mdsymlem5  29965  sat1el2xp  32186  nn0prpwlem  33188  axc11n11r  33524  broucube  34364  rngoueqz  34657  rngonegrmul  34661  zerdivemp1x  34664  lshpdisj  35565  linepsubN  36330  pmapsub  36346  paddasslem5  36402  dalaw  36464  pclclN  36469  pclfinN  36478  trlval2  36741  tendospcanN  37601  diaintclN  37636  dibintclN  37745  dihintcl  37922  dvh4dimlem  38021  com3rgbi  40264  2reu8i  42716  ssfz12  42918  iccpartlt  42954  iccelpart  42963  iccpartnel  42968  fargshiftf1  42971  fargshiftfva  42973  sbcpr  43049  reuopreuprim  43054  lighneallem3  43138  lighneal  43142  sbgoldbwt  43308  isomuspgrlem2b  43360  nzerooringczr  43705  lindslinindsimp1  43877