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  5463  po2ne  5556  fveqdmss  7032  resf1extb  7886  tfrlem9  8326  omordi  8503  nnmordi  8569  fundmen  8980  pssnn  9105  fiint  9239  infssuni  9258  cfcoflem  10194  fin1a2lem10  10331  axdc3lem2  10373  zorn2lem7  10424  fpwwe2lem11  10564  genpnnp  10928  mulgt0sr  11028  nn01to3  12866  fzdif1  13533  elfzodifsumelfzo  13659  ssfzo12  13687  elfznelfzo  13701  injresinjlem  13718  injresinj  13719  ssnn0fi  13920  expcan  14104  ltexp2  14105  hashgt12el2  14358  fi1uzind  14442  swrdswrdlem  14639  swrdswrd  14640  wrd2ind  14658  swrdccatin1  14660  cshwlen  14734  2cshwcshw  14760  cshwcsh2id  14763  dvdsmodexp  16199  dvdsaddre2b  16246  lcmfunsnlem2lem1  16577  lcmfdvdsb  16582  coprmproddvdslem  16601  infpnlem1  16850  cshwshashlem1  17035  initoeu1  17947  initoeu2lem1  17950  initoeu2  17952  termoeu1  17954  grpinveu  18916  mulgass2  20256  lss1d  20926  nzerooringczr  21447  cply1mul  22252  gsummoncoe1  22264  mp2pm2mplem4  22765  chpscmat  22798  chcoeffeq  22842  cnpnei  23220  hausnei2  23309  cmpsublem  23355  comppfsc  23488  filufint  23876  flimopn  23931  flimrest  23939  alexsubALTlem3  24005  equivcfil  25267  dvfsumrlim3  26008  pntlem3  27588  elntg2  29070  numedglnl  29229  cusgrsize2inds  29539  2pthnloop  29816  usgr2wlkneq  29841  elwspths2on  30047  elwspths2onw  30048  clwwlkccatlem  30076  clwlkclwwlklem2a  30085  clwwisshclwws  30102  erclwwlktr  30109  erclwwlkntr  30158  3cyclfrgrrn1  30372  vdgn1frgrv2  30383  frgrncvvdeqlem8  30393  frgrwopreglem5  30408  frgrwopreglem5ALT  30409  frgr2wwlkeqm  30418  2clwwlk2clwwlk  30437  frgrregord013  30482  grpoinveu  30606  elspansn4  31660  atomli  32469  mdsymlem3  32492  mdsymlem5  32494  sat1el2xp  35592  satffunlem  35614  satffunlem1lem1  35615  satffunlem2lem1  35617  nn0prpwlem  36535  axc11n11r  36925  broucube  37902  rngoueqz  38188  rngonegrmul  38192  zerdivemp1x  38195  lshpdisj  39360  linepsubN  40125  pmapsub  40141  paddasslem5  40197  dalaw  40259  pclclN  40264  pclfinN  40273  trlval2  40536  tendospcanN  41396  diaintclN  41431  dibintclN  41540  dihintcl  41717  dvh4dimlem  41816  com3rgbi  44867  2reu8i  47470  ssfz12  47671  iccpartlt  47781  iccelpart  47790  iccpartnel  47795  fargshiftf1  47798  fargshiftfva  47800  sbcpr  47878  reuopreuprim  47883  lighneallem3  47964  lighneal  47968  sbgoldbwt  48134  grimcnv  48245  grimco  48246  isuspgrimlem  48252  uhgrimisgrgriclem  48287  grimedg  48292  cycl3grtri  48304  isubgr3stgrlem6  48328  grlicsym  48370  clnbgr3stgrgrlic  48377  pgnbgreunbgrlem3  48475  pgnbgreunbgrlem6  48481  lindslinindsimp1  48814