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  5491  po2ne  5586  fveqdmss  7074  resf1extb  7930  tfrlem9  8371  omordi  8550  nnmordi  8616  fundmen  9027  pssnn  9152  fiint  9285  infssuni  9302  cfcoflem  10255  fin1a2lem10  10392  axdc3lem2  10434  zorn2lem7  10485  fpwwe2lem11  10625  genpnnp  10989  mulgt0sr  11089  nn01to3  12964  fzdif1  13632  elfzodifsumelfzo  13759  ssfzo12  13787  elfznelfzo  13801  injresinjlem  13818  injresinj  13819  ssnn0fi  14020  expcan  14204  ltexp2  14205  hashgt12el2  14459  fi1uzind  14543  swrdswrdlem  14740  swrdswrd  14741  wrd2ind  14759  swrdccatin1  14761  cshwlen  14835  2cshwcshw  14861  cshwcsh2id  14864  dvdsmodexp  16317  dvdsaddre2b  16364  lcmfunsnlem2lem1  16695  lcmfdvdsb  16700  coprmproddvdslem  16719  infpnlem1  16969  cshwshashlem1  17154  initoeu1  18067  initoeu2lem1  18070  initoeu2  18072  termoeu1  18074  grpinveu  19040  mulgass2  20391  lss1d  21061  nzerooringczr  21598  cply1mul  22424  gsummoncoe1  22436  mp2pm2mplem4  22934  chpscmat  22967  chcoeffeq  23011  cnpnei  23389  hausnei2  23478  cmpsublem  23524  comppfsc  23657  filufint  24045  flimopn  24100  flimrest  24108  alexsubALTlem3  24174  equivcfil  25426  dvfsumrlim3  26160  pntlem3  27738  elntg2  29275  numedglnl  29434  cusgrsize2inds  29743  2pthnloop  30020  usgr2wlkneq  30045  elwspths2on  30251  elwspths2onw  30252  clwwlkccatlem  30280  clwlkclwwlklem2a  30289  clwwisshclwws  30306  erclwwlktr  30313  erclwwlkntr  30362  3cyclfrgrrn1  30576  vdgn1frgrv2  30587  frgrncvvdeqlem8  30597  frgrwopreglem5  30612  frgrwopreglem5ALT  30613  frgr2wwlkeqm  30622  2clwwlk2clwwlk  30641  frgrregord013  30686  grpoinveu  30811  elspansn4  31865  atomli  32674  mdsymlem3  32697  mdsymlem5  32699  sat1el2xp  35769  satffunlem  35791  satffunlem1lem1  35792  satffunlem2lem1  35794  nn0prpwlem  36721  axc11n11r  37196  broucube  38192  rngoueqz  38478  rngonegrmul  38482  zerdivemp1x  38485  lshpdisj  39650  linepsubN  40415  pmapsub  40431  paddasslem5  40487  dalaw  40549  pclclN  40554  pclfinN  40563  trlval2  40826  tendospcanN  41686  diaintclN  41721  dibintclN  41830  dihintcl  42007  dvh4dimlem  42106  com3rgbi  45114  2reu8i  47738  ssfz12  47939  iccpartlt  48061  iccelpart  48070  iccpartnel  48075  fargshiftf1  48078  fargshiftfva  48080  sbcpr  48158  reuopreuprim  48163  lighneallem3  48247  lighneal  48251  sbgoldbwt  48430  grimcnv  48541  grimco  48542  isuspgrimlem  48548  uhgrimisgrgriclem  48583  grimedg  48588  cycl3grtri  48600  isubgr3stgrlem6  48624  grlicsym  48666  clnbgr3stgrgrlic  48673  pgnbgreunbgrlem3  48771  pgnbgreunbgrlem6  48777  lindslinindsimp1  49121