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 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜓 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com25  100  propeqop  5484  po2ne  5579  fveqdmss  7071  resf1extb  7931  tfrlem9  8374  omordi  8553  nnmordi  8619  fundmen  9038  pssnn  9163  fiint  9296  infssuni  9313  cfcoflem  10274  fin1a2lem10  10411  axdc3lem2  10453  zorn2lem7  10504  fpwwe2lem11  10650  genpnnp  11014  mulgt0sr  11114  nn01to3  12990  fzdif1  13660  elfzodifsumelfzo  13787  ssfzo12  13815  elfznelfzo  13829  injresinjlem  13846  injresinj  13847  ssnn0fi  14049  expcan  14233  ltexp2  14234  hashgt12el2  14488  fi1uzind  14572  swrdswrdlem  14773  swrdswrd  14774  wrd2ind  14792  swrdccatin1  14794  cshwlen  14870  2cshwcshw  14896  cshwcsh2id  14899  dvdsmodexp  16350  dvdsaddre2b  16397  lcmfunsnlem2lem1  16728  lcmfdvdsb  16733  coprmproddvdslem  16752  infpnlem1  17002  cshwshashlem1  17187  initoeu1  18100  initoeu2lem1  18103  initoeu2  18105  termoeu1  18107  grpinveu  19098  mulgass2  20451  lss1d  21147  nzerooringczr  21693  cply1mul  22521  gsummoncoe1  22533  mp2pm2mplem4  23034  chpscmat  23067  chcoeffeq  23111  cnpnei  23489  hausnei2  23578  cmpsublem  23624  comppfsc  23758  filufint  24146  flimopn  24201  flimrest  24209  alexsubALTlem3  24275  equivcfil  25527  dvfsumrlim3  26260  pntlem3  27845  elntg2  29442  numedglnl  29601  cusgrsize2inds  29913  2pthnloop  30196  usgr2wlkneq  30221  elwspths2on  30430  elwspths2onw  30431  clwwlkccatlem  30459  clwlkclwwlklem2a  30468  clwwisshclwws  30485  erclwwlktr  30492  erclwwlkntr  30541  3cyclfrgrrn1  30765  vdgn1frgrv2  30776  frgrncvvdeqlem8  30786  frgrwopreglem5  30801  frgrwopreglem5ALT  30802  frgr2wwlkeqm  30811  2clwwlk2clwwlk  30830  frgrregord013  30875  grpoinveu  31000  elspansn4  32054  atomli  32863  mdsymlem3  32886  mdsymlem5  32888  sat1el2xp  35958  satffunlem  35980  satffunlem1lem1  35981  satffunlem2lem1  35983  nn0prpwlem  36941  axc11n11r  37416  broucube  38403  rngoueqz  38690  rngonegrmul  38694  zerdivemp1x  38697  lshpdisj  39860  linepsubN  40625  pmapsub  40641  paddasslem5  40697  dalaw  40759  pclclN  40764  pclfinN  40773  trlval2  41036  tendospcanN  41896  diaintclN  41931  dibintclN  42040  dihintcl  42217  dvh4dimlem  42316  com3rgbi  45337  2reu8i  48001  ssfz12  48202  iccpartlt  48324  iccelpart  48333  iccpartnel  48338  fargshiftf1  48341  fargshiftfva  48343  sbcpr  48421  reuopreuprim  48426  lighneallem3  48510  lighneal  48514  sbgoldbwt  48693  grimcnv  48804  grimco  48805  isuspgrimlem  48811  uhgrimisgrgriclem  48846  grimedg  48851  cycl3grtri  48863  isubgr3stgrlem6  48887  grlicsym  48929  clnbgr3stgrgrlic  48936  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040  lindslinindsimp1  49387