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  5478  po2ne  5574  fveqdmss  7079  resf1extb  7947  tfrlem9  8397  omordi  8578  nnmordi  8644  fundmen  9063  pssnn  9188  fiint  9322  infssuni  9339  cfcoflem  10354  fin1a2lem10  10491  axdc3lem2  10533  zorn2lem7  10584  fpwwe2lem11  10730  genpnnp  11094  mulgt0sr  11194  nn01to3  13072  fzdif1  13743  elfzodifsumelfzo  13870  ssfzo12  13898  elfznelfzo  13912  injresinjlem  13929  injresinj  13930  ssnn0fi  14132  expcan  14316  ltexp2  14317  hashgt12el2  14572  fi1uzind  14656  swrdswrdlem  14858  swrdswrd  14859  wrd2ind  14877  swrdccatin1  14879  cshwlen  14955  2cshwcshw  14981  cshwcsh2id  14984  dvdsmodexp  16436  dvdsaddre2b  16483  lcmfunsnlem2lem1  16819  lcmfdvdsb  16824  coprmproddvdslem  16843  infpnlem1  17094  cshwshashlem1  17279  initoeu1  18192  initoeu2lem1  18195  initoeu2  18197  termoeu1  18199  grpinveu  19191  mulgass2  20546  lss1d  21244  nzerooringczr  21792  cply1mul  22620  gsummoncoe1  22632  mp2pm2mplem4  23133  chpscmat  23166  chcoeffeq  23210  cnpnei  23588  hausnei2  23677  cmpsublem  23723  comppfsc  23857  filufint  24245  flimopn  24300  flimrest  24308  alexsubALTlem3  24374  equivcfil  25626  dvfsumrlim3  26359  pntlem3  27942  elntg2  29569  numedglnl  29728  cusgrsize2inds  30040  2pthnloop  30323  usgr2wlkneq  30348  elwspths2on  30557  elwspths2onw  30558  clwwlkccatlem  30586  clwlkclwwlklem2a  30595  clwwisshclwws  30612  erclwwlktr  30619  erclwwlkntr  30668  3cyclfrgrrn1  30892  vdgn1frgrv2  30903  frgrncvvdeqlem8  30913  frgrwopreglem5  30928  frgrwopreglem5ALT  30929  frgr2wwlkeqm  30938  2clwwlk2clwwlk  30957  frgrregord013  31002  grpoinveu  31127  elspansn4  32181  atomli  32990  mdsymlem3  33013  mdsymlem5  33015  sat1el2xp  36231  satffunlem  36253  satffunlem1lem1  36254  satffunlem2lem1  36256  nn0prpwlem  37203  axc11n11r  37678  broucube  38666  rngoueqz  38968  rngonegrmul  38972  zerdivemp1x  38975  lshpdisj  40138  linepsubN  40903  pmapsub  40919  paddasslem5  40975  dalaw  41037  pclclN  41042  pclfinN  41051  trlval2  41314  tendospcanN  42174  diaintclN  42209  dibintclN  42318  dihintcl  42495  dvh4dimlem  42594  com3rgbi  45591  2reu8i  48277  ssfz12  48478  iccpartlt  48600  iccelpart  48609  iccpartnel  48614  fargshiftf1  48617  fargshiftfva  48619  sbcpr  48697  reuopreuprim  48702  lighneallem3  48786  lighneal  48790  sbgoldbwt  48969  grimcnv  49080  grimco  49081  isuspgrimlem  49087  uhgrimisgrgriclem  49122  grimedg  49127  cycl3grtri  49139  isubgr3stgrlem6  49163  grlicsym  49205  clnbgr3stgrgrlic  49212  pgnbgreunbgrlem3  49310  pgnbgreunbgrlem6  49316  lindslinindsimp1  49663