Theorem com24 93

Description: Commutation of antecedents. Swap 2nd and 4th. Deduction associated with com13 86. (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 91	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com13 86	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  97  imim12  103  propeqop  4895  predpo  5615  fveqdmss  6262  tfrlem9  7368  omordi  7533  nnmordi  7598  fundmen  7916  pssnn  8063  fiint  8122  infssuni  8140  cfcoflem  8977  fin1a2lem10  9114  axdc3lem2  9156  zorn2lem7  9207  fpwwe2lem12  9342  genpnnp  9706  mulgt0sr  9805  nn01to3  11657  elfzodifsumelfzo  12401  ssfzo12  12427  elfznelfzo  12439  injresinjlem  12450  injresinj  12451  ssnn0fi  12646  expcan  12775  ltexp2  12776  hashgt12el2  13071  fundmge2nop0  13129  fi1uzind  13134  fi1uzindOLD  13140  swrdswrdlem  13311  swrdswrd  13312  wrd2ind  13329  swrdccatin1  13334  cshwlen  13396  2cshwcshw  13422  cshwcsh2id  13425  dvdsaddre2b  14867  lcmfunsnlem2lem1  15189  lcmfdvdsb  15194  coprmproddvdslem  15214  infpnlem1  15452  cshwshashlem1  15640  initoeu1  16484  initoeu2lem1  16487  initoeu2  16489  termoeu1  16491  grpinveu  17279  mulgass2  18424  lss1d  18784  cply1mul  19485  gsummoncoe1  19495  mp2pm2mplem4  20433  chpscmat  20466  chcoeffeq  20510  cnpnei  20878  hausnei2  20967  cmpsublem  21012  comppfsc  21145  filufint  21534  flimopn  21589  flimrest  21597  alexsubALTlem3  21663  equivcfil  22905  dvfsumrlim3  23600  pntlem3  25098  nbcusgra  25992  cusgrasize2inds  26005  usgrasscusgra  26011  cyclnspth  26159  fargshiftf1  26165  fargshiftfva  26167  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  wlkiswwlk1  26218  clwwlkgt0  26299  clwlkisclwwlklem2a  26313  erclwwlktr  26343  erclwwlkntr  26355  el2wlkonot  26396  el2spthonot  26397  usg2wlkonot  26410  usg2wotspth  26411  rusgrasn  26472  eupatrl  26495  frgraunss  26522  3cyclfrgrarn1  26539  3cyclfrgrarn  26540  vdfrgra0  26549  vdgn0frgrav2  26551  vdgn1frgrav2  26553  frgrancvvdeqlemB  26565  frgrawopreglem2  26572  frgrawopreglem5  26575  usg2spot2nb  26592  numclwwlkovf2ex  26613  frgrareggt1  26643  frgrareg  26644  frgraregord013  26645  grpoinveu  26757  elspansn4  27816  atomli  28625  mdsymlem3  28648  mdsymlem5  28650  nn0prpwlem  31487  axc11n11r  31860  broucube  32613  rngoueqz  32909  rngonegrmul  32913  zerdivemp1x  32916  lshpdisj  33292  linepsubN  34056  pmapsub  34072  paddasslem5  34128  dalaw  34190  pclclN  34195  pclfinN  34204  trlval2  34468  tendospcanN  35330  diaintclN  35365  dibintclN  35474  dihintcl  35651  dvh4dimlem  35750  com3rgbi  37741  iccpartlt  39962  iccelpart  39971  iccpartnel  39976  lighneallem3  40062  lighneal  40066  bgoldbwt  40199  ssfz12  40351  cusgrsize2inds  40669  2pthnloop  40937  usgr2wlkneq  40962  elwspths2on  41163  clwlkclwwlklem2a  41207  clwwisshclwws  41235  erclwwlkstr  41243  erclwwlksntr  41255  clwlksfclwwlk  41269  3cyclfrgrrn1  41455  vdgn1frgrv2  41466  frgrncvvdeqlemB  41477  frgrwopreglem5  41485  av-numclwwlkovf2ex  41517  av-frgraregord013  41549  nzerooringczr  41864  lindslinindsimp1  42040