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  5397  po2ne  5489  predpo  6166  fveqdmss  6846  tfrlem9  8021  omordi  8192  nnmordi  8257  fundmen  8583  pssnn  8736  fiint  8795  infssuni  8815  cfcoflem  9694  fin1a2lem10  9831  axdc3lem2  9873  zorn2lem7  9924  fpwwe2lem12  10063  genpnnp  10427  mulgt0sr  10527  nn01to3  12342  elfzodifsumelfzo  13104  ssfzo12  13131  elfznelfzo  13143  injresinjlem  13158  injresinj  13159  ssnn0fi  13354  expcan  13534  ltexp2  13535  hashgt12el2  13785  fi1uzind  13856  swrdswrdlem  14066  swrdswrd  14067  wrd2ind  14085  swrdccatin1  14087  cshwlen  14161  2cshwcshw  14187  cshwcsh2id  14190  dvdsmodexp  15615  dvdsaddre2b  15657  lcmfunsnlem2lem1  15982  lcmfdvdsb  15987  coprmproddvdslem  16006  infpnlem1  16246  cshwshashlem1  16429  initoeu1  17271  initoeu2lem1  17274  initoeu2  17276  termoeu1  17278  grpinveu  18138  mulgass2  19351  lss1d  19735  cply1mul  20462  gsummoncoe1  20472  mp2pm2mplem4  21417  chpscmat  21450  chcoeffeq  21494  cnpnei  21872  hausnei2  21961  cmpsublem  22007  comppfsc  22140  filufint  22528  flimopn  22583  flimrest  22591  alexsubALTlem3  22657  equivcfil  23902  dvfsumrlim3  24630  pntlem3  26185  elntg2  26771  numedglnl  26929  cusgrsize2inds  27235  2pthnloop  27512  usgr2wlkneq  27537  elwspths2on  27739  clwwlkccatlem  27767  clwlkclwwlklem2a  27776  clwwisshclwws  27793  erclwwlktr  27800  erclwwlkntr  27850  3cyclfrgrrn1  28064  vdgn1frgrv2  28075  frgrncvvdeqlem8  28085  frgrwopreglem5  28100  frgrwopreglem5ALT  28101  frgr2wwlkeqm  28110  2clwwlk2clwwlk  28129  frgrregord013  28174  grpoinveu  28296  elspansn4  29350  atomli  30159  mdsymlem3  30182  mdsymlem5  30184  sat1el2xp  32626  satffunlem  32648  satffunlem1lem1  32649  satffunlem2lem1  32651  nn0prpwlem  33670  axc11n11r  34017  broucube  34941  rngoueqz  35233  rngonegrmul  35237  zerdivemp1x  35240  lshpdisj  36138  linepsubN  36903  pmapsub  36919  paddasslem5  36975  dalaw  37037  pclclN  37042  pclfinN  37051  trlval2  37314  tendospcanN  38174  diaintclN  38209  dibintclN  38318  dihintcl  38495  dvh4dimlem  38594  com3rgbi  40897  2reu8i  43361  ssfz12  43563  iccpartlt  43633  iccelpart  43642  iccpartnel  43647  fargshiftf1  43650  fargshiftfva  43652  sbcpr  43732  reuopreuprim  43737  lighneallem3  43821  lighneal  43825  sbgoldbwt  43991  isomuspgrlem2b  44043  nzerooringczr  44392  lindslinindsimp1  44561