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  5473  po2ne  5567  fveqdmss  7054  resf1extb  7910  tfrlem9  8350  omordi  8529  nnmordi  8595  fundmen  9006  pssnn  9131  fiint  9265  infssuni  9283  cfcoflem  10223  fin1a2lem10  10360  axdc3lem2  10402  zorn2lem7  10453  fpwwe2lem11  10593  genpnnp  10957  mulgt0sr  11057  nn01to3  12936  fzdif1  13604  elfzodifsumelfzo  13731  ssfzo12  13759  elfznelfzo  13773  injresinjlem  13790  injresinj  13791  ssnn0fi  13992  expcan  14176  ltexp2  14177  hashgt12el2  14430  fi1uzind  14514  swrdswrdlem  14711  swrdswrd  14712  wrd2ind  14730  swrdccatin1  14732  cshwlen  14806  2cshwcshw  14832  cshwcsh2id  14835  dvdsmodexp  16285  dvdsaddre2b  16332  lcmfunsnlem2lem1  16663  lcmfdvdsb  16668  coprmproddvdslem  16687  infpnlem1  16937  cshwshashlem1  17122  initoeu1  18035  initoeu2lem1  18038  initoeu2  18040  termoeu1  18042  grpinveu  19007  mulgass2  20346  lss1d  21018  nzerooringczr  21520  cply1mul  22347  gsummoncoe1  22359  mp2pm2mplem4  22857  chpscmat  22890  chcoeffeq  22934  cnpnei  23312  hausnei2  23401  cmpsublem  23447  comppfsc  23580  filufint  23968  flimopn  24023  flimrest  24031  alexsubALTlem3  24097  equivcfil  25349  dvfsumrlim3  26083  pntlem3  27661  elntg2  29143  numedglnl  29302  cusgrsize2inds  29611  2pthnloop  29888  usgr2wlkneq  29913  elwspths2on  30119  elwspths2onw  30120  clwwlkccatlem  30148  clwlkclwwlklem2a  30157  clwwisshclwws  30174  erclwwlktr  30181  erclwwlkntr  30230  3cyclfrgrrn1  30444  vdgn1frgrv2  30455  frgrncvvdeqlem8  30465  frgrwopreglem5  30480  frgrwopreglem5ALT  30481  frgr2wwlkeqm  30490  2clwwlk2clwwlk  30509  frgrregord013  30554  grpoinveu  30679  elspansn4  31733  atomli  32542  mdsymlem3  32565  mdsymlem5  32567  sat1el2xp  35690  satffunlem  35712  satffunlem1lem1  35713  satffunlem2lem1  35715  nn0prpwlem  36643  axc11n11r  37119  broucube  38114  rngoueqz  38400  rngonegrmul  38404  zerdivemp1x  38407  lshpdisj  39572  linepsubN  40337  pmapsub  40353  paddasslem5  40409  dalaw  40471  pclclN  40476  pclfinN  40485  trlval2  40748  tendospcanN  41608  diaintclN  41643  dibintclN  41752  dihintcl  41929  dvh4dimlem  42028  com3rgbi  45051  2reu8i  47668  ssfz12  47869  iccpartlt  47991  iccelpart  48000  iccpartnel  48005  fargshiftf1  48008  fargshiftfva  48010  sbcpr  48088  reuopreuprim  48093  lighneallem3  48177  lighneal  48181  sbgoldbwt  48360  grimcnv  48471  grimco  48472  isuspgrimlem  48478  uhgrimisgrgriclem  48513  grimedg  48518  cycl3grtri  48530  isubgr3stgrlem6  48554  grlicsym  48596  clnbgr3stgrgrlic  48603  pgnbgreunbgrlem3  48701  pgnbgreunbgrlem6  48707  lindslinindsimp1  49040