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  5455  po2ne  5548  fveqdmss  7024  resf1extb  7878  tfrlem9  8317  omordi  8494  nnmordi  8560  fundmen  8971  pssnn  9096  fiint  9230  infssuni  9249  cfcoflem  10185  fin1a2lem10  10322  axdc3lem2  10364  zorn2lem7  10415  fpwwe2lem11  10555  genpnnp  10919  mulgt0sr  11019  nn01to3  12882  fzdif1  13550  elfzodifsumelfzo  13677  ssfzo12  13705  elfznelfzo  13719  injresinjlem  13736  injresinj  13737  ssnn0fi  13938  expcan  14122  ltexp2  14123  hashgt12el2  14376  fi1uzind  14460  swrdswrdlem  14657  swrdswrd  14658  wrd2ind  14676  swrdccatin1  14678  cshwlen  14752  2cshwcshw  14778  cshwcsh2id  14781  dvdsmodexp  16220  dvdsaddre2b  16267  lcmfunsnlem2lem1  16598  lcmfdvdsb  16603  coprmproddvdslem  16622  infpnlem1  16872  cshwshashlem1  17057  initoeu1  17969  initoeu2lem1  17972  initoeu2  17974  termoeu1  17976  grpinveu  18941  mulgass2  20281  lss1d  20949  nzerooringczr  21470  cply1mul  22271  gsummoncoe1  22283  mp2pm2mplem4  22784  chpscmat  22817  chcoeffeq  22861  cnpnei  23239  hausnei2  23328  cmpsublem  23374  comppfsc  23507  filufint  23895  flimopn  23950  flimrest  23958  alexsubALTlem3  24024  equivcfil  25276  dvfsumrlim3  26010  pntlem3  27586  elntg2  29068  numedglnl  29227  cusgrsize2inds  29537  2pthnloop  29814  usgr2wlkneq  29839  elwspths2on  30045  elwspths2onw  30046  clwwlkccatlem  30074  clwlkclwwlklem2a  30083  clwwisshclwws  30100  erclwwlktr  30107  erclwwlkntr  30156  3cyclfrgrrn1  30370  vdgn1frgrv2  30381  frgrncvvdeqlem8  30391  frgrwopreglem5  30406  frgrwopreglem5ALT  30407  frgr2wwlkeqm  30416  2clwwlk2clwwlk  30435  frgrregord013  30480  grpoinveu  30605  elspansn4  31659  atomli  32468  mdsymlem3  32491  mdsymlem5  32493  sat1el2xp  35577  satffunlem  35599  satffunlem1lem1  35600  satffunlem2lem1  35602  nn0prpwlem  36520  axc11n11r  36996  broucube  37989  rngoueqz  38275  rngonegrmul  38279  zerdivemp1x  38282  lshpdisj  39447  linepsubN  40212  pmapsub  40228  paddasslem5  40284  dalaw  40346  pclclN  40351  pclfinN  40360  trlval2  40623  tendospcanN  41483  diaintclN  41518  dibintclN  41627  dihintcl  41804  dvh4dimlem  41903  com3rgbi  44959  2reu8i  47573  ssfz12  47774  iccpartlt  47896  iccelpart  47905  iccpartnel  47910  fargshiftf1  47913  fargshiftfva  47915  sbcpr  47993  reuopreuprim  47998  lighneallem3  48082  lighneal  48086  sbgoldbwt  48265  grimcnv  48376  grimco  48377  isuspgrimlem  48383  uhgrimisgrgriclem  48418  grimedg  48423  cycl3grtri  48435  isubgr3stgrlem6  48459  grlicsym  48501  clnbgr3stgrgrlic  48508  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem6  48612  lindslinindsimp1  48945