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  5482  po2ne  5577  fveqdmss  7068  resf1extb  7930  tfrlem9  8399  omordi  8578  nnmordi  8643  fundmen  9045  pssnn  9182  fiint  9338  fiintOLD  9339  infssuni  9358  cfcoflem  10286  fin1a2lem10  10423  axdc3lem2  10465  zorn2lem7  10516  fpwwe2lem11  10655  genpnnp  11019  mulgt0sr  11119  nn01to3  12957  fzdif1  13622  elfzodifsumelfzo  13747  ssfzo12  13775  elfznelfzo  13788  injresinjlem  13803  injresinj  13804  ssnn0fi  14003  expcan  14187  ltexp2  14188  hashgt12el2  14441  fi1uzind  14525  swrdswrdlem  14722  swrdswrd  14723  wrd2ind  14741  swrdccatin1  14743  cshwlen  14817  2cshwcshw  14844  cshwcsh2id  14847  dvdsmodexp  16280  dvdsaddre2b  16326  lcmfunsnlem2lem1  16657  lcmfdvdsb  16662  coprmproddvdslem  16681  infpnlem1  16930  cshwshashlem1  17115  initoeu1  18024  initoeu2lem1  18027  initoeu2  18029  termoeu1  18031  grpinveu  18957  mulgass2  20269  lss1d  20920  nzerooringczr  21441  cply1mul  22234  gsummoncoe1  22246  mp2pm2mplem4  22747  chpscmat  22780  chcoeffeq  22824  cnpnei  23202  hausnei2  23291  cmpsublem  23337  comppfsc  23470  filufint  23858  flimopn  23913  flimrest  23921  alexsubALTlem3  23987  equivcfil  25251  dvfsumrlim3  25992  pntlem3  27572  elntg2  28964  numedglnl  29123  cusgrsize2inds  29433  2pthnloop  29713  usgr2wlkneq  29738  elwspths2on  29942  clwwlkccatlem  29970  clwlkclwwlklem2a  29979  clwwisshclwws  29996  erclwwlktr  30003  erclwwlkntr  30052  3cyclfrgrrn1  30266  vdgn1frgrv2  30277  frgrncvvdeqlem8  30287  frgrwopreglem5  30302  frgrwopreglem5ALT  30303  frgr2wwlkeqm  30312  2clwwlk2clwwlk  30331  frgrregord013  30376  grpoinveu  30500  elspansn4  31554  atomli  32363  mdsymlem3  32386  mdsymlem5  32388  sat1el2xp  35401  satffunlem  35423  satffunlem1lem1  35424  satffunlem2lem1  35426  nn0prpwlem  36340  axc11n11r  36701  broucube  37678  rngoueqz  37964  rngonegrmul  37968  zerdivemp1x  37971  lshpdisj  39005  linepsubN  39771  pmapsub  39787  paddasslem5  39843  dalaw  39905  pclclN  39910  pclfinN  39919  trlval2  40182  tendospcanN  41042  diaintclN  41077  dibintclN  41186  dihintcl  41363  dvh4dimlem  41462  com3rgbi  44539  2reu8i  47142  ssfz12  47343  iccpartlt  47438  iccelpart  47447  iccpartnel  47452  fargshiftf1  47455  fargshiftfva  47457  sbcpr  47535  reuopreuprim  47540  lighneallem3  47621  lighneal  47625  sbgoldbwt  47791  grimcnv  47901  grimco  47902  isuspgrimlem  47908  uhgrimisgrgriclem  47943  grimedg  47948  cycl3grtri  47959  isubgr3stgrlem6  47983  grlicsym  48018  clnbgr3stgrgrlic  48024  lindslinindsimp1  48433