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  5442  po2ne  5535  fveqdmss  7006  resf1extb  7859  tfrlem9  8299  omordi  8476  nnmordi  8541  fundmen  8948  pssnn  9073  fiint  9206  infssuni  9225  cfcoflem  10158  fin1a2lem10  10295  axdc3lem2  10337  zorn2lem7  10388  fpwwe2lem11  10527  genpnnp  10891  mulgt0sr  10991  nn01to3  12834  fzdif1  13500  elfzodifsumelfzo  13626  ssfzo12  13654  elfznelfzo  13668  injresinjlem  13685  injresinj  13686  ssnn0fi  13887  expcan  14071  ltexp2  14072  hashgt12el2  14325  fi1uzind  14409  swrdswrdlem  14606  swrdswrd  14607  wrd2ind  14625  swrdccatin1  14627  cshwlen  14701  2cshwcshw  14727  cshwcsh2id  14730  dvdsmodexp  16166  dvdsaddre2b  16213  lcmfunsnlem2lem1  16544  lcmfdvdsb  16549  coprmproddvdslem  16568  infpnlem1  16817  cshwshashlem1  17002  initoeu1  17913  initoeu2lem1  17916  initoeu2  17918  termoeu1  17920  grpinveu  18882  mulgass2  20222  lss1d  20891  nzerooringczr  21412  cply1mul  22206  gsummoncoe1  22218  mp2pm2mplem4  22719  chpscmat  22752  chcoeffeq  22796  cnpnei  23174  hausnei2  23263  cmpsublem  23309  comppfsc  23442  filufint  23830  flimopn  23885  flimrest  23893  alexsubALTlem3  23959  equivcfil  25221  dvfsumrlim3  25962  pntlem3  27542  elntg2  28958  numedglnl  29117  cusgrsize2inds  29427  2pthnloop  29704  usgr2wlkneq  29729  elwspths2on  29933  clwwlkccatlem  29961  clwlkclwwlklem2a  29970  clwwisshclwws  29987  erclwwlktr  29994  erclwwlkntr  30043  3cyclfrgrrn1  30257  vdgn1frgrv2  30268  frgrncvvdeqlem8  30278  frgrwopreglem5  30293  frgrwopreglem5ALT  30294  frgr2wwlkeqm  30303  2clwwlk2clwwlk  30322  frgrregord013  30367  grpoinveu  30491  elspansn4  31545  atomli  32354  mdsymlem3  32377  mdsymlem5  32379  sat1el2xp  35415  satffunlem  35437  satffunlem1lem1  35438  satffunlem2lem1  35440  nn0prpwlem  36356  axc11n11r  36717  broucube  37694  rngoueqz  37980  rngonegrmul  37984  zerdivemp1x  37987  lshpdisj  39026  linepsubN  39791  pmapsub  39807  paddasslem5  39863  dalaw  39925  pclclN  39930  pclfinN  39939  trlval2  40202  tendospcanN  41062  diaintclN  41097  dibintclN  41206  dihintcl  41383  dvh4dimlem  41482  com3rgbi  44547  2reu8i  47144  ssfz12  47345  iccpartlt  47455  iccelpart  47464  iccpartnel  47469  fargshiftf1  47472  fargshiftfva  47474  sbcpr  47552  reuopreuprim  47557  lighneallem3  47638  lighneal  47642  sbgoldbwt  47808  grimcnv  47919  grimco  47920  isuspgrimlem  47926  uhgrimisgrgriclem  47961  grimedg  47966  cycl3grtri  47978  isubgr3stgrlem6  48002  grlicsym  48044  clnbgr3stgrgrlic  48051  pgnbgreunbgrlem3  48149  pgnbgreunbgrlem6  48155  lindslinindsimp1  48489