Theorem com24 96

Description: Commutation of antecedents. Swap 2nd and 4th. Deduction associated with com13 89. (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 94	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com13 89	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  100  propeqop  5488  po2ne  5583  fveqdmss  7071  resf1extb  7927  tfrlem9  8368  omordi  8547  nnmordi  8613  fundmen  9024  pssnn  9149  fiint  9282  infssuni  9299  cfcoflem  10252  fin1a2lem10  10389  axdc3lem2  10431  zorn2lem7  10482  fpwwe2lem11  10622  genpnnp  10986  mulgt0sr  11086  nn01to3  12961  fzdif1  13629  elfzodifsumelfzo  13756  ssfzo12  13784  elfznelfzo  13798  injresinjlem  13815  injresinj  13816  ssnn0fi  14017  expcan  14201  ltexp2  14202  hashgt12el2  14456  fi1uzind  14540  swrdswrdlem  14737  swrdswrd  14738  wrd2ind  14756  swrdccatin1  14758  cshwlen  14832  2cshwcshw  14858  cshwcsh2id  14861  dvdsmodexp  16314  dvdsaddre2b  16361  lcmfunsnlem2lem1  16692  lcmfdvdsb  16697  coprmproddvdslem  16716  infpnlem1  16966  cshwshashlem1  17151  initoeu1  18064  initoeu2lem1  18067  initoeu2  18069  termoeu1  18071  grpinveu  19037  mulgass2  20388  lss1d  21058  nzerooringczr  21595  cply1mul  22421  gsummoncoe1  22433  mp2pm2mplem4  22931  chpscmat  22964  chcoeffeq  23008  cnpnei  23386  hausnei2  23475  cmpsublem  23521  comppfsc  23654  filufint  24042  flimopn  24097  flimrest  24105  alexsubALTlem3  24171  equivcfil  25423  dvfsumrlim3  26157  pntlem3  27735  elntg2  29272  numedglnl  29431  cusgrsize2inds  29740  2pthnloop  30017  usgr2wlkneq  30042  elwspths2on  30248  elwspths2onw  30249  clwwlkccatlem  30277  clwlkclwwlklem2a  30286  clwwisshclwws  30303  erclwwlktr  30310  erclwwlkntr  30359  3cyclfrgrrn1  30573  vdgn1frgrv2  30584  frgrncvvdeqlem8  30594  frgrwopreglem5  30609  frgrwopreglem5ALT  30610  frgr2wwlkeqm  30619  2clwwlk2clwwlk  30638  frgrregord013  30683  grpoinveu  30808  elspansn4  31862  atomli  32671  mdsymlem3  32694  mdsymlem5  32696  sat1el2xp  35766  satffunlem  35788  satffunlem1lem1  35789  satffunlem2lem1  35791  nn0prpwlem  36718  axc11n11r  37193  broucube  38188  rngoueqz  38474  rngonegrmul  38478  zerdivemp1x  38481  lshpdisj  39646  linepsubN  40411  pmapsub  40427  paddasslem5  40483  dalaw  40545  pclclN  40550  pclfinN  40559  trlval2  40822  tendospcanN  41682  diaintclN  41717  dibintclN  41826  dihintcl  42003  dvh4dimlem  42102  com3rgbi  45108  2reu8i  47732  ssfz12  47933  iccpartlt  48055  iccelpart  48064  iccpartnel  48069  fargshiftf1  48072  fargshiftfva  48074  sbcpr  48152  reuopreuprim  48157  lighneallem3  48241  lighneal  48245  sbgoldbwt  48424  grimcnv  48535  grimco  48536  isuspgrimlem  48542  uhgrimisgrgriclem  48577  grimedg  48582  cycl3grtri  48594  isubgr3stgrlem6  48618  grlicsym  48660  clnbgr3stgrgrlic  48667  pgnbgreunbgrlem3  48765  pgnbgreunbgrlem6  48771  lindslinindsimp1  49115