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  5492  po2ne  5587  fveqdmss  7075  resf1extb  7932  tfrlem9  8373  omordi  8552  nnmordi  8618  fundmen  9029  pssnn  9154  fiint  9287  infssuni  9304  cfcoflem  10257  fin1a2lem10  10394  axdc3lem2  10436  zorn2lem7  10487  fpwwe2lem11  10627  genpnnp  10991  mulgt0sr  11091  nn01to3  12966  fzdif1  13635  elfzodifsumelfzo  13762  ssfzo12  13790  elfznelfzo  13804  injresinjlem  13821  injresinj  13822  ssnn0fi  14023  expcan  14207  ltexp2  14208  hashgt12el2  14462  fi1uzind  14546  swrdswrdlem  14743  swrdswrd  14744  wrd2ind  14762  swrdccatin1  14764  cshwlen  14838  2cshwcshw  14864  cshwcsh2id  14867  dvdsmodexp  16319  dvdsaddre2b  16366  lcmfunsnlem2lem1  16697  lcmfdvdsb  16702  coprmproddvdslem  16721  infpnlem1  16971  cshwshashlem1  17156  initoeu1  18069  initoeu2lem1  18072  initoeu2  18074  termoeu1  18076  grpinveu  19042  mulgass2  20393  lss1d  21065  nzerooringczr  21611  cply1mul  22437  gsummoncoe1  22449  mp2pm2mplem4  22947  chpscmat  22980  chcoeffeq  23024  cnpnei  23402  hausnei2  23491  cmpsublem  23537  comppfsc  23670  filufint  24058  flimopn  24113  flimrest  24121  alexsubALTlem3  24187  equivcfil  25439  dvfsumrlim3  26173  pntlem3  27754  elntg2  29316  numedglnl  29475  cusgrsize2inds  29784  2pthnloop  30061  usgr2wlkneq  30086  elwspths2on  30292  elwspths2onw  30293  clwwlkccatlem  30321  clwlkclwwlklem2a  30330  clwwisshclwws  30347  erclwwlktr  30354  erclwwlkntr  30403  3cyclfrgrrn1  30617  vdgn1frgrv2  30628  frgrncvvdeqlem8  30638  frgrwopreglem5  30653  frgrwopreglem5ALT  30654  frgr2wwlkeqm  30663  2clwwlk2clwwlk  30682  frgrregord013  30727  grpoinveu  30852  elspansn4  31906  atomli  32715  mdsymlem3  32738  mdsymlem5  32740  sat1el2xp  35852  satffunlem  35874  satffunlem1lem1  35875  satffunlem2lem1  35877  nn0prpwlem  36814  axc11n11r  37289  broucube  38286  rngoueqz  38572  rngonegrmul  38576  zerdivemp1x  38579  lshpdisj  39742  linepsubN  40507  pmapsub  40523  paddasslem5  40579  dalaw  40641  pclclN  40646  pclfinN  40655  trlval2  40918  tendospcanN  41778  diaintclN  41813  dibintclN  41922  dihintcl  42099  dvh4dimlem  42198  com3rgbi  45206  2reu8i  47833  ssfz12  48034  iccpartlt  48156  iccelpart  48165  iccpartnel  48170  fargshiftf1  48173  fargshiftfva  48175  sbcpr  48253  reuopreuprim  48258  lighneallem3  48342  lighneal  48346  sbgoldbwt  48525  grimcnv  48636  grimco  48637  isuspgrimlem  48643  uhgrimisgrgriclem  48678  grimedg  48683  cycl3grtri  48695  isubgr3stgrlem6  48719  grlicsym  48761  clnbgr3stgrgrlic  48768  pgnbgreunbgrlem3  48866  pgnbgreunbgrlem6  48872  lindslinindsimp1  49220