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  5470  po2ne  5565  fveqdmss  7053  resf1extb  7913  tfrlem9  8356  omordi  8533  nnmordi  8598  fundmen  9005  pssnn  9138  fiint  9284  fiintOLD  9285  infssuni  9304  cfcoflem  10232  fin1a2lem10  10369  axdc3lem2  10411  zorn2lem7  10462  fpwwe2lem11  10601  genpnnp  10965  mulgt0sr  11065  nn01to3  12907  fzdif1  13573  elfzodifsumelfzo  13699  ssfzo12  13727  elfznelfzo  13740  injresinjlem  13755  injresinj  13756  ssnn0fi  13957  expcan  14141  ltexp2  14142  hashgt12el2  14395  fi1uzind  14479  swrdswrdlem  14676  swrdswrd  14677  wrd2ind  14695  swrdccatin1  14697  cshwlen  14771  2cshwcshw  14798  cshwcsh2id  14801  dvdsmodexp  16237  dvdsaddre2b  16284  lcmfunsnlem2lem1  16615  lcmfdvdsb  16620  coprmproddvdslem  16639  infpnlem1  16888  cshwshashlem1  17073  initoeu1  17980  initoeu2lem1  17983  initoeu2  17985  termoeu1  17987  grpinveu  18913  mulgass2  20225  lss1d  20876  nzerooringczr  21397  cply1mul  22190  gsummoncoe1  22202  mp2pm2mplem4  22703  chpscmat  22736  chcoeffeq  22780  cnpnei  23158  hausnei2  23247  cmpsublem  23293  comppfsc  23426  filufint  23814  flimopn  23869  flimrest  23877  alexsubALTlem3  23943  equivcfil  25206  dvfsumrlim3  25947  pntlem3  27527  elntg2  28919  numedglnl  29078  cusgrsize2inds  29388  2pthnloop  29668  usgr2wlkneq  29693  elwspths2on  29897  clwwlkccatlem  29925  clwlkclwwlklem2a  29934  clwwisshclwws  29951  erclwwlktr  29958  erclwwlkntr  30007  3cyclfrgrrn1  30221  vdgn1frgrv2  30232  frgrncvvdeqlem8  30242  frgrwopreglem5  30257  frgrwopreglem5ALT  30258  frgr2wwlkeqm  30267  2clwwlk2clwwlk  30286  frgrregord013  30331  grpoinveu  30455  elspansn4  31509  atomli  32318  mdsymlem3  32341  mdsymlem5  32343  sat1el2xp  35373  satffunlem  35395  satffunlem1lem1  35396  satffunlem2lem1  35398  nn0prpwlem  36317  axc11n11r  36678  broucube  37655  rngoueqz  37941  rngonegrmul  37945  zerdivemp1x  37948  lshpdisj  38987  linepsubN  39753  pmapsub  39769  paddasslem5  39825  dalaw  39887  pclclN  39892  pclfinN  39901  trlval2  40164  tendospcanN  41024  diaintclN  41059  dibintclN  41168  dihintcl  41345  dvh4dimlem  41444  com3rgbi  44511  2reu8i  47118  ssfz12  47319  iccpartlt  47429  iccelpart  47438  iccpartnel  47443  fargshiftf1  47446  fargshiftfva  47448  sbcpr  47526  reuopreuprim  47531  lighneallem3  47612  lighneal  47616  sbgoldbwt  47782  grimcnv  47892  grimco  47893  isuspgrimlem  47899  uhgrimisgrgriclem  47934  grimedg  47939  cycl3grtri  47950  isubgr3stgrlem6  47974  grlicsym  48009  clnbgr3stgrgrlic  48015  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  lindslinindsimp1  48450