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  5517  po2ne  5613  fveqdmss  7098  tfrlem9  8424  omordi  8603  nnmordi  8668  fundmen  9070  pssnn  9207  fiint  9364  fiintOLD  9365  infssuni  9384  cfcoflem  10310  fin1a2lem10  10447  axdc3lem2  10489  zorn2lem7  10540  fpwwe2lem11  10679  genpnnp  11043  mulgt0sr  11143  nn01to3  12981  fzdif1  13642  elfzodifsumelfzo  13767  ssfzo12  13795  elfznelfzo  13808  injresinjlem  13823  injresinj  13824  ssnn0fi  14023  expcan  14206  ltexp2  14207  hashgt12el2  14459  fi1uzind  14543  swrdswrdlem  14739  swrdswrd  14740  wrd2ind  14758  swrdccatin1  14760  cshwlen  14834  2cshwcshw  14861  cshwcsh2id  14864  dvdsmodexp  16295  dvdsaddre2b  16341  lcmfunsnlem2lem1  16672  lcmfdvdsb  16677  coprmproddvdslem  16696  infpnlem1  16944  cshwshashlem1  17130  initoeu1  18065  initoeu2lem1  18068  initoeu2  18070  termoeu1  18072  grpinveu  19005  mulgass2  20323  lss1d  20979  nzerooringczr  21509  cply1mul  22316  gsummoncoe1  22328  mp2pm2mplem4  22831  chpscmat  22864  chcoeffeq  22908  cnpnei  23288  hausnei2  23377  cmpsublem  23423  comppfsc  23556  filufint  23944  flimopn  23999  flimrest  24007  alexsubALTlem3  24073  equivcfil  25347  dvfsumrlim3  26089  pntlem3  27668  elntg2  29015  numedglnl  29176  cusgrsize2inds  29486  2pthnloop  29764  usgr2wlkneq  29789  elwspths2on  29990  clwwlkccatlem  30018  clwlkclwwlklem2a  30027  clwwisshclwws  30044  erclwwlktr  30051  erclwwlkntr  30100  3cyclfrgrrn1  30314  vdgn1frgrv2  30325  frgrncvvdeqlem8  30335  frgrwopreglem5  30350  frgrwopreglem5ALT  30351  frgr2wwlkeqm  30360  2clwwlk2clwwlk  30379  frgrregord013  30424  grpoinveu  30548  elspansn4  31602  atomli  32411  mdsymlem3  32434  mdsymlem5  32436  sat1el2xp  35364  satffunlem  35386  satffunlem1lem1  35387  satffunlem2lem1  35389  nn0prpwlem  36305  axc11n11r  36666  broucube  37641  rngoueqz  37927  rngonegrmul  37931  zerdivemp1x  37934  lshpdisj  38969  linepsubN  39735  pmapsub  39751  paddasslem5  39807  dalaw  39869  pclclN  39874  pclfinN  39883  trlval2  40146  tendospcanN  41006  diaintclN  41041  dibintclN  41150  dihintcl  41327  dvh4dimlem  41426  com3rgbi  44512  2reu8i  47063  ssfz12  47264  iccpartlt  47349  iccelpart  47358  iccpartnel  47363  fargshiftf1  47366  fargshiftfva  47368  sbcpr  47446  reuopreuprim  47451  lighneallem3  47532  lighneal  47536  sbgoldbwt  47702  isuspgrimlem  47812  grimcnv  47817  grimco  47818  uhgrimisgrgriclem  47836  grimedg  47841  isubgr3stgrlem6  47874  grlicsym  47909  clnbgr3stgrgrlic  47915  lindslinindsimp1  48303