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  propeqop  5461  po2ne  5555  fveqdmss  7030  resf1extb  7885  tfrlem9  8324  omordi  8501  nnmordi  8567  fundmen  8978  pssnn  9103  fiint  9237  infssuni  9256  cfcoflem  10194  fin1a2lem10  10331  axdc3lem2  10373  zorn2lem7  10424  fpwwe2lem11  10564  genpnnp  10928  mulgt0sr  11028  nn01to3  12891  fzdif1  13559  elfzodifsumelfzo  13686  ssfzo12  13714  elfznelfzo  13728  injresinjlem  13745  injresinj  13746  ssnn0fi  13947  expcan  14131  ltexp2  14132  hashgt12el2  14385  fi1uzind  14469  swrdswrdlem  14666  swrdswrd  14667  wrd2ind  14685  swrdccatin1  14687  cshwlen  14761  2cshwcshw  14787  cshwcsh2id  14790  dvdsmodexp  16229  dvdsaddre2b  16276  lcmfunsnlem2lem1  16607  lcmfdvdsb  16612  coprmproddvdslem  16631  infpnlem1  16881  cshwshashlem1  17066  initoeu1  17978  initoeu2lem1  17981  initoeu2  17983  termoeu1  17985  grpinveu  18950  mulgass2  20290  lss1d  20958  nzerooringczr  21460  cply1mul  22261  gsummoncoe1  22273  mp2pm2mplem4  22774  chpscmat  22807  chcoeffeq  22851  cnpnei  23229  hausnei2  23318  cmpsublem  23364  comppfsc  23497  filufint  23885  flimopn  23940  flimrest  23948  alexsubALTlem3  24014  equivcfil  25266  dvfsumrlim3  26000  pntlem3  27572  elntg2  29054  numedglnl  29213  cusgrsize2inds  29522  2pthnloop  29799  usgr2wlkneq  29824  elwspths2on  30030  elwspths2onw  30031  clwwlkccatlem  30059  clwlkclwwlklem2a  30068  clwwisshclwws  30085  erclwwlktr  30092  erclwwlkntr  30141  3cyclfrgrrn1  30355  vdgn1frgrv2  30366  frgrncvvdeqlem8  30376  frgrwopreglem5  30391  frgrwopreglem5ALT  30392  frgr2wwlkeqm  30401  2clwwlk2clwwlk  30420  frgrregord013  30465  grpoinveu  30590  elspansn4  31644  atomli  32453  mdsymlem3  32476  mdsymlem5  32478  sat1el2xp  35561  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  nn0prpwlem  36504  axc11n11r  36980  broucube  37975  rngoueqz  38261  rngonegrmul  38265  zerdivemp1x  38268  lshpdisj  39433  linepsubN  40198  pmapsub  40214  paddasslem5  40270  dalaw  40332  pclclN  40337  pclfinN  40346  trlval2  40609  tendospcanN  41469  diaintclN  41504  dibintclN  41613  dihintcl  41790  dvh4dimlem  41889  com3rgbi  44941  2reu8i  47561  ssfz12  47762  iccpartlt  47884  iccelpart  47893  iccpartnel  47898  fargshiftf1  47901  fargshiftfva  47903  sbcpr  47981  reuopreuprim  47986  lighneallem3  48070  lighneal  48074  sbgoldbwt  48253  grimcnv  48364  grimco  48365  isuspgrimlem  48371  uhgrimisgrgriclem  48406  grimedg  48411  cycl3grtri  48423  isubgr3stgrlem6  48447  grlicsym  48489  clnbgr3stgrgrlic  48496  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  lindslinindsimp1  48933