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  5467  po2ne  5562  fveqdmss  7050  resf1extb  7910  tfrlem9  8353  omordi  8530  nnmordi  8595  fundmen  9002  pssnn  9132  fiint  9277  fiintOLD  9278  infssuni  9297  cfcoflem  10225  fin1a2lem10  10362  axdc3lem2  10404  zorn2lem7  10455  fpwwe2lem11  10594  genpnnp  10958  mulgt0sr  11058  nn01to3  12900  fzdif1  13566  elfzodifsumelfzo  13692  ssfzo12  13720  elfznelfzo  13733  injresinjlem  13748  injresinj  13749  ssnn0fi  13950  expcan  14134  ltexp2  14135  hashgt12el2  14388  fi1uzind  14472  swrdswrdlem  14669  swrdswrd  14670  wrd2ind  14688  swrdccatin1  14690  cshwlen  14764  2cshwcshw  14791  cshwcsh2id  14794  dvdsmodexp  16230  dvdsaddre2b  16277  lcmfunsnlem2lem1  16608  lcmfdvdsb  16613  coprmproddvdslem  16632  infpnlem1  16881  cshwshashlem1  17066  initoeu1  17973  initoeu2lem1  17976  initoeu2  17978  termoeu1  17980  grpinveu  18906  mulgass2  20218  lss1d  20869  nzerooringczr  21390  cply1mul  22183  gsummoncoe1  22195  mp2pm2mplem4  22696  chpscmat  22729  chcoeffeq  22773  cnpnei  23151  hausnei2  23240  cmpsublem  23286  comppfsc  23419  filufint  23807  flimopn  23862  flimrest  23870  alexsubALTlem3  23936  equivcfil  25199  dvfsumrlim3  25940  pntlem3  27520  elntg2  28912  numedglnl  29071  cusgrsize2inds  29381  2pthnloop  29661  usgr2wlkneq  29686  elwspths2on  29890  clwwlkccatlem  29918  clwlkclwwlklem2a  29927  clwwisshclwws  29944  erclwwlktr  29951  erclwwlkntr  30000  3cyclfrgrrn1  30214  vdgn1frgrv2  30225  frgrncvvdeqlem8  30235  frgrwopreglem5  30250  frgrwopreglem5ALT  30251  frgr2wwlkeqm  30260  2clwwlk2clwwlk  30279  frgrregord013  30324  grpoinveu  30448  elspansn4  31502  atomli  32311  mdsymlem3  32334  mdsymlem5  32336  sat1el2xp  35366  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  nn0prpwlem  36310  axc11n11r  36671  broucube  37648  rngoueqz  37934  rngonegrmul  37938  zerdivemp1x  37941  lshpdisj  38980  linepsubN  39746  pmapsub  39762  paddasslem5  39818  dalaw  39880  pclclN  39885  pclfinN  39894  trlval2  40157  tendospcanN  41017  diaintclN  41052  dibintclN  41161  dihintcl  41338  dvh4dimlem  41437  com3rgbi  44504  2reu8i  47114  ssfz12  47315  iccpartlt  47425  iccelpart  47434  iccpartnel  47439  fargshiftf1  47442  fargshiftfva  47444  sbcpr  47522  reuopreuprim  47527  lighneallem3  47608  lighneal  47612  sbgoldbwt  47778  grimcnv  47888  grimco  47889  isuspgrimlem  47895  uhgrimisgrgriclem  47930  grimedg  47935  cycl3grtri  47946  isubgr3stgrlem6  47970  grlicsym  48005  clnbgr3stgrgrlic  48011  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  lindslinindsimp1  48446