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  5434  po2ne  5530  fveqdmss  6988  tfrlem9  8247  omordi  8428  nnmordi  8493  fundmen  8856  pssnn  8989  pssnnOLD  9084  fiint  9135  infssuni  9154  cfcoflem  10074  fin1a2lem10  10211  axdc3lem2  10253  zorn2lem7  10304  fpwwe2lem11  10443  genpnnp  10807  mulgt0sr  10907  nn01to3  12727  elfzodifsumelfzo  13499  ssfzo12  13526  elfznelfzo  13538  injresinjlem  13553  injresinj  13554  ssnn0fi  13751  expcan  13933  ltexp2  13934  hashgt12el2  14183  fi1uzind  14256  swrdswrdlem  14462  swrdswrd  14463  wrd2ind  14481  swrdccatin1  14483  cshwlen  14557  2cshwcshw  14583  cshwcsh2id  14586  dvdsmodexp  16016  dvdsaddre2b  16061  lcmfunsnlem2lem1  16388  lcmfdvdsb  16393  coprmproddvdslem  16412  infpnlem1  16656  cshwshashlem1  16842  initoeu1  17771  initoeu2lem1  17774  initoeu2  17776  termoeu1  17778  grpinveu  18659  mulgass2  19885  lss1d  20270  cply1mul  21510  gsummoncoe1  21520  mp2pm2mplem4  22003  chpscmat  22036  chcoeffeq  22080  cnpnei  22460  hausnei2  22549  cmpsublem  22595  comppfsc  22728  filufint  23116  flimopn  23171  flimrest  23179  alexsubALTlem3  23245  equivcfil  24508  dvfsumrlim3  25242  pntlem3  26802  elntg2  27398  numedglnl  27559  cusgrsize2inds  27865  2pthnloop  28144  usgr2wlkneq  28169  elwspths2on  28370  clwwlkccatlem  28398  clwlkclwwlklem2a  28407  clwwisshclwws  28424  erclwwlktr  28431  erclwwlkntr  28480  3cyclfrgrrn1  28694  vdgn1frgrv2  28705  frgrncvvdeqlem8  28715  frgrwopreglem5  28730  frgrwopreglem5ALT  28731  frgr2wwlkeqm  28740  2clwwlk2clwwlk  28759  frgrregord013  28804  grpoinveu  28926  elspansn4  29980  atomli  30789  mdsymlem3  30812  mdsymlem5  30814  sat1el2xp  33386  satffunlem  33408  satffunlem1lem1  33409  satffunlem2lem1  33411  nn0prpwlem  34556  axc11n11r  34910  broucube  35855  rngoueqz  36142  rngonegrmul  36146  zerdivemp1x  36149  lshpdisj  37043  linepsubN  37808  pmapsub  37824  paddasslem5  37880  dalaw  37942  pclclN  37947  pclfinN  37956  trlval2  38219  tendospcanN  39079  diaintclN  39114  dibintclN  39223  dihintcl  39400  dvh4dimlem  39499  com3rgbi  42172  2reu8i  44663  ssfz12  44864  iccpartlt  44934  iccelpart  44943  iccpartnel  44948  fargshiftf1  44951  fargshiftfva  44953  sbcpr  45031  reuopreuprim  45036  lighneallem3  45117  lighneal  45121  sbgoldbwt  45287  isomuspgrlem2b  45339  nzerooringczr  45688  lindslinindsimp1  45856