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  5399  po2ne  5491  predpo  6168  fveqdmss  6848  tfrlem9  8023  omordi  8194  nnmordi  8259  fundmen  8585  pssnn  8738  fiint  8797  infssuni  8817  cfcoflem  9696  fin1a2lem10  9833  axdc3lem2  9875  zorn2lem7  9926  fpwwe2lem12  10065  genpnnp  10429  mulgt0sr  10529  nn01to3  12344  elfzodifsumelfzo  13106  ssfzo12  13133  elfznelfzo  13145  injresinjlem  13160  injresinj  13161  ssnn0fi  13356  expcan  13536  ltexp2  13537  hashgt12el2  13787  fi1uzind  13858  swrdswrdlem  14068  swrdswrd  14069  wrd2ind  14087  swrdccatin1  14089  cshwlen  14163  2cshwcshw  14189  cshwcsh2id  14192  dvdsmodexp  15617  dvdsaddre2b  15659  lcmfunsnlem2lem1  15984  lcmfdvdsb  15989  coprmproddvdslem  16008  infpnlem1  16248  cshwshashlem1  16431  initoeu1  17273  initoeu2lem1  17276  initoeu2  17278  termoeu1  17280  grpinveu  18140  mulgass2  19353  lss1d  19737  cply1mul  20464  gsummoncoe1  20474  mp2pm2mplem4  21419  chpscmat  21452  chcoeffeq  21496  cnpnei  21874  hausnei2  21963  cmpsublem  22009  comppfsc  22142  filufint  22530  flimopn  22585  flimrest  22593  alexsubALTlem3  22659  equivcfil  23904  dvfsumrlim3  24632  pntlem3  26187  elntg2  26773  numedglnl  26931  cusgrsize2inds  27237  2pthnloop  27514  usgr2wlkneq  27539  elwspths2on  27741  clwwlkccatlem  27769  clwlkclwwlklem2a  27778  clwwisshclwws  27795  erclwwlktr  27802  erclwwlkntr  27852  3cyclfrgrrn1  28066  vdgn1frgrv2  28077  frgrncvvdeqlem8  28087  frgrwopreglem5  28102  frgrwopreglem5ALT  28103  frgr2wwlkeqm  28112  2clwwlk2clwwlk  28131  frgrregord013  28176  grpoinveu  28298  elspansn4  29352  atomli  30161  mdsymlem3  30184  mdsymlem5  30186  sat1el2xp  32628  satffunlem  32650  satffunlem1lem1  32651  satffunlem2lem1  32653  nn0prpwlem  33672  axc11n11r  34019  broucube  34928  rngoueqz  35220  rngonegrmul  35224  zerdivemp1x  35227  lshpdisj  36125  linepsubN  36890  pmapsub  36906  paddasslem5  36962  dalaw  37024  pclclN  37029  pclfinN  37038  trlval2  37301  tendospcanN  38161  diaintclN  38196  dibintclN  38305  dihintcl  38482  dvh4dimlem  38581  com3rgbi  40855  2reu8i  43319  ssfz12  43521  iccpartlt  43591  iccelpart  43600  iccpartnel  43605  fargshiftf1  43608  fargshiftfva  43610  sbcpr  43690  reuopreuprim  43695  lighneallem3  43779  lighneal  43783  sbgoldbwt  43949  isomuspgrlem2b  44001  nzerooringczr  44350  lindslinindsimp1  44519