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  5508  po2ne  5605  fveqdmss  7081  tfrlem9  8385  omordi  8566  nnmordi  8631  fundmen  9031  pssnn  9168  pssnnOLD  9265  fiint  9324  infssuni  9343  cfcoflem  10267  fin1a2lem10  10404  axdc3lem2  10446  zorn2lem7  10497  fpwwe2lem11  10636  genpnnp  11000  mulgt0sr  11100  nn01to3  12925  elfzodifsumelfzo  13698  ssfzo12  13725  elfznelfzo  13737  injresinjlem  13752  injresinj  13753  ssnn0fi  13950  expcan  14134  ltexp2  14135  hashgt12el2  14383  fi1uzind  14458  swrdswrdlem  14654  swrdswrd  14655  wrd2ind  14673  swrdccatin1  14675  cshwlen  14749  2cshwcshw  14776  cshwcsh2id  14779  dvdsmodexp  16205  dvdsaddre2b  16250  lcmfunsnlem2lem1  16575  lcmfdvdsb  16580  coprmproddvdslem  16599  infpnlem1  16843  cshwshashlem1  17029  initoeu1  17961  initoeu2lem1  17964  initoeu2  17966  termoeu1  17968  grpinveu  18859  mulgass2  20121  lss1d  20574  cply1mul  21818  gsummoncoe1  21828  mp2pm2mplem4  22311  chpscmat  22344  chcoeffeq  22388  cnpnei  22768  hausnei2  22857  cmpsublem  22903  comppfsc  23036  filufint  23424  flimopn  23479  flimrest  23487  alexsubALTlem3  23553  equivcfil  24816  dvfsumrlim3  25550  pntlem3  27112  elntg2  28274  numedglnl  28435  cusgrsize2inds  28741  2pthnloop  29019  usgr2wlkneq  29044  elwspths2on  29245  clwwlkccatlem  29273  clwlkclwwlklem2a  29282  clwwisshclwws  29299  erclwwlktr  29306  erclwwlkntr  29355  3cyclfrgrrn1  29569  vdgn1frgrv2  29580  frgrncvvdeqlem8  29590  frgrwopreglem5  29605  frgrwopreglem5ALT  29606  frgr2wwlkeqm  29615  2clwwlk2clwwlk  29634  frgrregord013  29679  grpoinveu  29803  elspansn4  30857  atomli  31666  mdsymlem3  31689  mdsymlem5  31691  sat1el2xp  34401  satffunlem  34423  satffunlem1lem1  34424  satffunlem2lem1  34426  nn0prpwlem  35255  axc11n11r  35609  broucube  36570  rngoueqz  36856  rngonegrmul  36860  zerdivemp1x  36863  lshpdisj  37905  linepsubN  38671  pmapsub  38687  paddasslem5  38743  dalaw  38805  pclclN  38810  pclfinN  38819  trlval2  39082  tendospcanN  39942  diaintclN  39977  dibintclN  40086  dihintcl  40263  dvh4dimlem  40362  com3rgbi  43323  2reu8i  45869  ssfz12  46070  iccpartlt  46140  iccelpart  46149  iccpartnel  46154  fargshiftf1  46157  fargshiftfva  46159  sbcpr  46237  reuopreuprim  46242  lighneallem3  46323  lighneal  46327  sbgoldbwt  46493  isomuspgrlem2b  46545  nzerooringczr  47018  lindslinindsimp1  47186