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  5375  po2ne  5469  predpo  6158  fveqdmss  6877  tfrlem9  8099  omordi  8272  nnmordi  8337  fundmen  8686  pssnn  8824  pssnnOLD  8872  fiint  8926  infssuni  8945  cfcoflem  9851  fin1a2lem10  9988  axdc3lem2  10030  zorn2lem7  10081  fpwwe2lem11  10220  genpnnp  10584  mulgt0sr  10684  nn01to3  12502  elfzodifsumelfzo  13273  ssfzo12  13300  elfznelfzo  13312  injresinjlem  13327  injresinj  13328  ssnn0fi  13523  expcan  13704  ltexp2  13705  hashgt12el2  13955  fi1uzind  14028  swrdswrdlem  14234  swrdswrd  14235  wrd2ind  14253  swrdccatin1  14255  cshwlen  14329  2cshwcshw  14355  cshwcsh2id  14358  dvdsmodexp  15786  dvdsaddre2b  15831  lcmfunsnlem2lem1  16158  lcmfdvdsb  16163  coprmproddvdslem  16182  infpnlem1  16426  cshwshashlem1  16612  initoeu1  17471  initoeu2lem1  17474  initoeu2  17476  termoeu1  17478  grpinveu  18356  mulgass2  19573  lss1d  19954  cply1mul  21169  gsummoncoe1  21179  mp2pm2mplem4  21660  chpscmat  21693  chcoeffeq  21737  cnpnei  22115  hausnei2  22204  cmpsublem  22250  comppfsc  22383  filufint  22771  flimopn  22826  flimrest  22834  alexsubALTlem3  22900  equivcfil  24150  dvfsumrlim3  24884  pntlem3  26444  elntg2  27030  numedglnl  27189  cusgrsize2inds  27495  2pthnloop  27772  usgr2wlkneq  27797  elwspths2on  27998  clwwlkccatlem  28026  clwlkclwwlklem2a  28035  clwwisshclwws  28052  erclwwlktr  28059  erclwwlkntr  28108  3cyclfrgrrn1  28322  vdgn1frgrv2  28333  frgrncvvdeqlem8  28343  frgrwopreglem5  28358  frgrwopreglem5ALT  28359  frgr2wwlkeqm  28368  2clwwlk2clwwlk  28387  frgrregord013  28432  grpoinveu  28554  elspansn4  29608  atomli  30417  mdsymlem3  30440  mdsymlem5  30442  sat1el2xp  33008  satffunlem  33030  satffunlem1lem1  33031  satffunlem2lem1  33033  nn0prpwlem  34197  axc11n11r  34551  broucube  35497  rngoueqz  35784  rngonegrmul  35788  zerdivemp1x  35791  lshpdisj  36687  linepsubN  37452  pmapsub  37468  paddasslem5  37524  dalaw  37586  pclclN  37591  pclfinN  37600  trlval2  37863  tendospcanN  38723  diaintclN  38758  dibintclN  38867  dihintcl  39044  dvh4dimlem  39143  com3rgbi  41748  2reu8i  44220  ssfz12  44422  iccpartlt  44492  iccelpart  44501  iccpartnel  44506  fargshiftf1  44509  fargshiftfva  44511  sbcpr  44589  reuopreuprim  44594  lighneallem3  44675  lighneal  44679  sbgoldbwt  44845  isomuspgrlem2b  44897  nzerooringczr  45246  lindslinindsimp1  45414