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  5486  po2ne  5582  fveqdmss  7110  resf1extb  7980  tfrlem9  8431  omordi  8612  nnmordi  8678  fundmen  9097  pssnn  9222  fiint  9356  infssuni  9373  cfcoflem  10389  fin1a2lem10  10526  axdc3lem2  10568  zorn2lem7  10619  fpwwe2lem11  10765  genpnnp  11129  mulgt0sr  11229  nn01to3  13108  fzdif1  13779  elfzodifsumelfzo  13906  ssfzo12  13934  elfznelfzo  13948  injresinjlem  13965  injresinj  13966  ssnn0fi  14168  expcan  14352  ltexp2  14353  hashgt12el2  14609  fi1uzind  14693  swrdswrdlem  14895  swrdswrd  14896  wrd2ind  14914  swrdccatin1  14916  cshwlen  14992  2cshwcshw  15018  cshwcsh2id  15021  dvdsmodexp  16474  dvdsaddre2b  16521  lcmfunsnlem2lem1  16857  lcmfdvdsb  16862  coprmproddvdslem  16881  infpnlem1  17132  cshwshashlem1  17317  initoeu1  18236  initoeu2lem1  18239  initoeu2  18241  termoeu1  18243  grpinveu  19235  mulgass2  20591  lss1d  21289  nzerooringczr  21841  cply1mul  22669  gsummoncoe1  22681  mp2pm2mplem4  23182  chpscmat  23215  chcoeffeq  23259  cnpnei  23637  hausnei2  23726  cmpsublem  23772  comppfsc  23906  filufint  24294  flimopn  24349  flimrest  24357  alexsubALTlem3  24423  equivcfil  25675  dvfsumrlim3  26408  pntlem3  27993  elntg2  29620  numedglnl  29779  cusgrsize2inds  30091  2pthnloop  30374  usgr2wlkneq  30399  elwspths2on  30608  elwspths2onw  30609  clwwlkccatlem  30637  clwlkclwwlklem2a  30646  clwwisshclwws  30663  erclwwlktr  30670  erclwwlkntr  30719  3cyclfrgrrn1  30943  vdgn1frgrv2  30954  frgrncvvdeqlem8  30964  frgrwopreglem5  30979  frgrwopreglem5ALT  30980  frgr2wwlkeqm  30989  2clwwlk2clwwlk  31008  frgrregord013  31053  grpoinveu  31178  elspansn4  32232  atomli  33041  mdsymlem3  33064  mdsymlem5  33066  sat1el2xp  36352  satffunlem  36374  satffunlem1lem1  36375  satffunlem2lem1  36377  nn0prpwlem  37325  axc11n11r  37800  broucube  38840  rngoueqz  39140  rngonegrmul  39144  zerdivemp1x  39147  lshpdisj  40310  linepsubN  41075  pmapsub  41091  paddasslem5  41147  dalaw  41209  pclclN  41214  pclfinN  41223  trlval2  41486  tendospcanN  42346  diaintclN  42381  dibintclN  42490  dihintcl  42667  dvh4dimlem  42766  com3rgbi  45757  2reu8i  48457  ssfz12  48657  iccpartlt  48779  iccelpart  48788  iccpartnel  48793  fargshiftf1  48796  fargshiftfva  48798  sbcpr  48876  reuopreuprim  48881  lighneallem3  48965  lighneal  48969  sbgoldbwt  49148  grimcnv  49259  grimco  49260  isuspgrimlem  49266  uhgrimisgrgriclem  49301  grimedg  49306  cycl3grtri  49318  isubgr3stgrlem6  49342  grlicsym  49384  clnbgr3stgrgrlic  49391  pgnbgreunbgrlem3  49489  pgnbgreunbgrlem6  49495  lindslinindsimp1  49900